<!DOCTYPE html>
<html class="writer-html5" lang="en" >
<head>
  <meta charset="utf-8" /><meta name="generator" content="Docutils 0.17.1: http://docutils.sourceforge.net/" />

  <meta name="viewport" content="width=device-width, initial-scale=1.0" />
  <title>8. Functions &mdash; The Mechanics of Proof, by Heather Macbeth</title>
      <link rel="stylesheet" href="_static/pygments.css" type="text/css" />
      <link rel="stylesheet" href="_static/css/theme.css" type="text/css" />
      <link rel="stylesheet" href="_static/css/custom.css" type="text/css" />
    <link rel="shortcut icon" href="_static/favicon.ico"/>
  <!--[if lt IE 9]>
    <script src="_static/js/html5shiv.min.js"></script>
  <![endif]-->
  
        <script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
        <script src="_static/jquery.js"></script>
        <script src="_static/underscore.js"></script>
        <script src="_static/doctools.js"></script>
        <script async="async" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
    <script src="_static/js/theme.js"></script>
    <link rel="index" title="Index" href="genindex.html" />
    <link rel="search" title="Search" href="search.html" />
    <link rel="next" title="9. Sets" href="09_Sets.html" />
    <link rel="prev" title="7. Number theory" href="07_Number_Theory.html" /> 
</head>

<body class="wy-body-for-nav"> 
  <div class="wy-grid-for-nav">
    <nav data-toggle="wy-nav-shift" class="wy-nav-side">
      <div class="wy-side-scroll">
        <div class="wy-side-nav-search" >
            <a href="index.html" class="icon icon-home"> The Mechanics of Proof
          </a>
<div role="search">
  <form id="rtd-search-form" class="wy-form" action="search.html" method="get">
    <input type="text" name="q" placeholder="Search docs" />
    <input type="hidden" name="check_keywords" value="yes" />
    <input type="hidden" name="area" value="default" />
  </form>
</div>
        </div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
              <ul>
<li class="toctree-l1"><a class="reference internal" href="00_Introduction.html">Preface</a></li>
</ul>
<ul class="current">
<li class="toctree-l1"><a class="reference internal" href="01_Proofs_by_Calculation.html">1. Proofs by calculation</a></li>
<li class="toctree-l1"><a class="reference internal" href="02_Proofs_with_Structure.html">2. Proofs with structure</a></li>
<li class="toctree-l1"><a class="reference internal" href="03_Parity_and_Divisibility.html">3. Parity and divisibility</a></li>
<li class="toctree-l1"><a class="reference internal" href="04_Proofs_with_Structure_II.html">4. Proofs with structure, II</a></li>
<li class="toctree-l1"><a class="reference internal" href="05_Logic.html">5. Logic</a></li>
<li class="toctree-l1"><a class="reference internal" href="06_Induction.html">6. Induction</a></li>
<li class="toctree-l1"><a class="reference internal" href="07_Number_Theory.html">7. Number theory</a></li>
<li class="toctree-l1 current"><a class="current reference internal" href="#">8. Functions</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#injectivity-and-surjectivity">8.1. Injectivity and surjectivity</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#example">8.1.1. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#definition">8.1.2. Definition</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id2">8.1.3. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#not-injective-example">8.1.4. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#surjective-def">8.1.5. Definition</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id5">8.1.6. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#not-surjective">8.1.7. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#musketeer">8.1.8. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id8">8.1.9. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#musketeer2">8.1.10. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id10">8.1.11. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id11">8.1.12. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#exercises">8.1.13. Exercises</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="#bijectivity">8.2. Bijectivity</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#id12">8.2.1. Definition</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id13">8.2.2. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id14">8.2.3. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#celestial-subatomic">8.2.4. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id16">8.2.5. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#bij-card2">8.2.6. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id18">8.2.7. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id19">8.2.8. Exercises</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="#composition-of-functions">8.3. Composition of functions</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#id20">8.3.1. Definition</a></li>
<li class="toctree-l3"><a class="reference internal" href="#ext">8.3.2. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id22">8.3.3. Definition</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id23">8.3.4. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id24">8.3.5. Definition</a></li>
<li class="toctree-l3"><a class="reference internal" href="#humour">8.3.6. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#bijective-to-inverse">8.3.7. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#inverse-to-bijection">8.3.8. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#bijective-iff-inverse">8.3.9. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id30">8.3.10. Exercises</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="#product-types">8.4. Product types</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#obtain-product">8.4.1. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#standard-plane-bij">8.4.2. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id34">8.4.3. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#injective-r2-r3">8.4.4. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id36">8.4.5. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id37">8.4.6. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id38">8.4.7. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id39">8.4.8. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id40">8.4.9. Example</a></li>
<li class="toctree-l3"><a class="reference internal" href="#id41">8.4.10. Exercises</a></li>
</ul>
</li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="09_Sets.html">9. Sets</a></li>
<li class="toctree-l1"><a class="reference internal" href="10_Relations.html">10. Relations</a></li>
</ul>
<ul>
<li class="toctree-l1"><a class="reference internal" href="Index_of_Tactics.html">Index of Lean tactics</a></li>
<li class="toctree-l1"><a class="reference internal" href="Mainstream_Lean.html">Transitioning to mainstream Lean</a></li>
</ul>

        </div>
      </div>
    </nav>

    <section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
          <i data-toggle="wy-nav-top" class="fa fa-bars"></i>
          <a href="index.html">The Mechanics of Proof</a>
      </nav>

      <div class="wy-nav-content">
        <div class="rst-content">
          <div role="navigation" aria-label="Page navigation">
  <ul class="wy-breadcrumbs">
      <li><a href="index.html" class="icon icon-home"></a> &raquo;</li>
      <li><span class="section-number">8. </span>Functions</li>
      <li class="wy-breadcrumbs-aside">
            <a href="_sources/08_Functions.rst.txt" rel="nofollow"> View page source</a>
      </li>
  </ul>
  <hr/>
</div>
          <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
           <div itemprop="articleBody">
             
  <section id="functions">
<span id="id1"></span><h1><span class="section-number">8. </span>Functions<a class="headerlink" href="#functions" title="Permalink to this headline">&#61633;</a></h1>
<p>So far in the book, we have studied properties of numbers (whether a number is odd,
positive, prime; whether one number is divisible by another) and operations on
numbers (addition, greatest common divisor).</p>
<p>In this chapter we go up a level of abstraction, and study properties of and
operations on functions.  These new properties include: whether a function is
<em>injective</em>, <em>surjective</em>, <em>bijective</em>; whether one function is <em>inverse</em> to
another; and the operation of <em>composition</em>.</p>
<p>We also expand our horizon beyond the numeric types (<span class="math notranslate nohighlight">\(\mathbb{N}\)</span>,
<span class="math notranslate nohighlight">\(\mathbb{Z}\)</span>, <span class="math notranslate nohighlight">\(\mathbb{Q}\)</span>, <span class="math notranslate nohighlight">\(\mathbb{R}\)</span>) which have formed the
setting of the early part of the book.  We now start to work with a broader range
of types, including function types, finite inductive types, and product types.</p>
<section id="injectivity-and-surjectivity">
<span id="inj-surj"></span><h2><span class="section-number">8.1. </span>Injectivity and surjectivity<a class="headerlink" href="#injectivity-and-surjectivity" title="Permalink to this headline">&#61633;</a></h2>
<section id="example">
<span id="functions-intro"></span><h3><span class="section-number">8.1.1. </span>Example<a class="headerlink" href="#example" title="Permalink to this headline">&#61633;</a></h3>
<p>We have studied particular functions before.  For example, the Fibonacci sequence from
<a class="reference internal" href="06_Induction.html#fibonacci"><span class="std std-numref">Example 6.3.3</span></a> is a function from <span class="math notranslate nohighlight">\(\mathbb{N}\)</span> to <span class="math notranslate nohighlight">\(\mathbb{Z}\)</span>: it
takes in a natural number, for example 5, and gives out an integer, in this case 8 (the index-5
term of the sequence).</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">F</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">&#8484;</span>
  <span class="bp">|</span> <span class="mi">0</span> <span class="bp">=&gt;</span> <span class="mi">1</span>
  <span class="bp">|</span> <span class="mi">1</span> <span class="bp">=&gt;</span> <span class="mi">1</span>
  <span class="bp">|</span> <span class="n">n</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">=&gt;</span> <span class="n">F</span> <span class="o">(</span><span class="n">n</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="bp">+</span> <span class="n">F</span> <span class="n">n</span>

<span class="k">#eval</span> <span class="n">F</span> <span class="mi">5</span> <span class="c1">-- infoview displays `8`</span>
</pre></div>
</div>
<p>The <em>domain</em> of a function is the type where it takes its input values, and the <em>codomain</em> of a
function is the type where it takes its output values.  For example, the domain of the Fibonacci
sequence is <span class="math notranslate nohighlight">\(\mathbb{N}\)</span> and its codomain is <span class="math notranslate nohighlight">\(\mathbb{Z}\)</span>.  The type of functions with
domain <span class="math notranslate nohighlight">\(\mathbb{N}\)</span> and codomain <span class="math notranslate nohighlight">\(\mathbb{Z}\)</span> is denoted
<span class="math notranslate nohighlight">\(\mathbb{N}\to \mathbb{Z}\)</span>.  Lean will confirm for us that the Fibonacci sequence <code class="docutils literal notranslate"><span class="pre">F</span></code> has
this type:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span> <span class="bp">@</span><span class="n">F</span> <span class="c1">-- infoview displays `F : &#8469; &#8594; &#8484;`</span>
</pre></div>
</div>
<p>Another way to define a function is by a closed formula.  For example,
&#8220;let <span class="math notranslate nohighlight">\(q:\mathbb{R}\to \mathbb{R}\)</span> be the function defined by, <span class="math notranslate nohighlight">\(q(x)=x+3\)</span>.&#8221;  In Lean we
can write this as</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">q</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="o">:=</span> <span class="n">x</span> <span class="bp">+</span> <span class="mi">3</span>
</pre></div>
</div>
<p>This function has domain <span class="math notranslate nohighlight">\(\mathbb{R}\)</span> and codomain <span class="math notranslate nohighlight">\(\mathbb{R}\)</span> &#8211; I even said when I
was defining it that I was making <span class="math notranslate nohighlight">\(q\)</span> to have type <span class="math notranslate nohighlight">\(\mathbb{R}\to \mathbb{R}\)</span>.  Let&#8217;s
check that this is indeed the type of the Lean object:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span> <span class="bp">@</span><span class="n">q</span> <span class="c1">-- infoview displays `q : &#8477; &#8594; &#8477;`</span>
</pre></div>
</div>
<p>A third way to define a function, if we expect to use it just once and don&#8217;t want to waste a name on
it, is by using the notation <span class="math notranslate nohighlight">\(\mapsto\)</span>: we can refer to &#8220;the function <span class="math notranslate nohighlight">\(x \mapsto x ^ 2\)</span>
from <span class="math notranslate nohighlight">\(\mathbb{R}\)</span> to <span class="math notranslate nohighlight">\(\mathbb{R}\)</span>&#8221;. Here is the same notation in Lean:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span> <span class="k">fun</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="c1">-- infoview displays `fun x &#8614; x ^ 2 : &#8477; &#8594; &#8477;`</span>
</pre></div>
</div>
</section>
<section id="definition">
<span id="injective-def"></span><h3><span class="section-number">8.1.2. </span>Definition<a class="headerlink" href="#definition" title="Permalink to this headline">&#61633;</a></h3>
<p>Now that we have the notation <span class="math notranslate nohighlight">\(X\to Y\)</span> for &#8220;the type of functions from <span class="math notranslate nohighlight">\(X\)</span> to
<span class="math notranslate nohighlight">\(Y\)</span>&#8221;, we can introduce properties of functions, in the same way that we have previously
introduced properties (like &#8220;odd&#8221; and &#8220;prime&#8221;) of numbers.  Here is our first one.</p>
<div class="admonition-definition admonition">
<p class="admonition-title">Definition</p>
<p>A function <span class="math notranslate nohighlight">\(f : X \to Y\)</span> is <em>injective</em>, if for all <span class="math notranslate nohighlight">\(x_1\)</span> and <span class="math notranslate nohighlight">\(x_2\)</span> of type
<span class="math notranslate nohighlight">\(X\)</span>, if <span class="math notranslate nohighlight">\(f(x_1)=f(x_2)\)</span>, then <span class="math notranslate nohighlight">\(x_1=x_2\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">Injective</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">)</span> <span class="o">:</span> <span class="kt">Prop</span> <span class="o">:=</span> <span class="bp">&#8704;</span> <span class="o">{</span><span class="n">x1</span> <span class="n">x2</span> <span class="o">:</span> <span class="n">X</span><span class="o">},</span> <span class="n">f</span> <span class="n">x1</span> <span class="bp">=</span> <span class="n">f</span> <span class="n">x2</span> <span class="bp">&#8594;</span> <span class="n">x1</span> <span class="bp">=</span> <span class="n">x2</span>
</pre></div>
</div>
</section>
<section id="id2">
<h3><span class="section-number">8.1.3. </span>Example<a class="headerlink" href="#id2" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that the function <span class="math notranslate nohighlight">\(q:\mathbb{R}\to\mathbb{R}\)</span> from
<a class="reference internal" href="#functions-intro"><span class="std std-numref">Example 8.1.1</span></a> is injective.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Let <span class="math notranslate nohighlight">\(x_1\)</span> and <span class="math notranslate nohighlight">\(x_2\)</span> be real numbers and suppose that <span class="math notranslate nohighlight">\(q(x_1)=q(x_2)\)</span>.  Then
<span class="math notranslate nohighlight">\(x_1+1=x_2+1\)</span>, so <span class="math notranslate nohighlight">\(x_1=x_2\)</span>.</p>
</div>
<p>Here is this solution in Lean.  Note that after unfolding the definition &#8220;injective&#8221; using the
command <code class="docutils literal notranslate"><span class="pre">dsimp</span> <span class="pre">[Injective]</span></code>, the goal state displays</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>&#8866; &#8704; &#10627;x1 x2 : &#8477;&#10628;, q x1 = q x2 &#8594; x1 = x2
</pre></div>
</div>
<p>This is the &#8220;injective&#8221; definition specialized to the problem at hand.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Injective</span> <span class="n">q</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Injective</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">x1</span> <span class="n">x2</span> <span class="n">h</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">q</span><span class="o">]</span> <span class="n">at</span> <span class="n">h</span>
  <span class="n">addarith</span> <span class="o">[</span><span class="n">h</span><span class="o">]</span>
</pre></div>
</div>
</section>
<section id="not-injective-example">
<span id="id3"></span><h3><span class="section-number">8.1.4. </span>Example<a class="headerlink" href="#not-injective-example" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that the function <span class="math notranslate nohighlight">\(x \mapsto x ^ 2\)</span> from <span class="math notranslate nohighlight">\(\mathbb{R}\)</span> to <span class="math notranslate nohighlight">\(\mathbb{R}\)</span>
is not injective.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We must show that there exist real numbers <span class="math notranslate nohighlight">\(x_1\)</span> and <span class="math notranslate nohighlight">\(x_2\)</span>, such that
<span class="math notranslate nohighlight">\(x_1{}^2=x_2{}^2\)</span> and <span class="math notranslate nohighlight">\(x_1\ne x_2\)</span>.  Indeed, -1 and 1 have these properties.</p>
</div>
<p>The first sentence of that proof was a negation-normalization: I unfolded the &#8220;injective&#8221; definition
and restated its negation in a logically equivalent but more convenient form.  Recall that in Lean
we do this using the tactic <code class="docutils literal notranslate"><span class="pre">push_neg</span></code>.  Here is the goal state after the tactic <code class="docutils literal notranslate"><span class="pre">push_neg</span></code> has
been used:</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>&#8866; &#8707; x1 x2, x1 ^ 2 = x2 ^ 2 &#8743; x1 &#8800; x2
</pre></div>
</div>
<p>And here is the full Lean proof.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Injective</span> <span class="o">(</span><span class="k">fun</span> <span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">&#8614;</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Injective</span><span class="o">]</span>
  <span class="n">push_neg</span>
  <span class="n">use</span> <span class="bp">-</span><span class="mi">1</span><span class="o">,</span> <span class="mi">1</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">numbers</span>
  <span class="bp">&#183;</span> <span class="n">numbers</span>
</pre></div>
</div>
</section>
<section id="surjective-def">
<span id="id4"></span><h3><span class="section-number">8.1.5. </span>Definition<a class="headerlink" href="#surjective-def" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-definition admonition">
<p class="admonition-title">Definition</p>
<p>A function <span class="math notranslate nohighlight">\(f : X \to Y\)</span> is <em>surjective</em>, if for all <span class="math notranslate nohighlight">\(y\)</span> of type <span class="math notranslate nohighlight">\(Y\)</span>, there
exists <span class="math notranslate nohighlight">\(x\)</span> of type <span class="math notranslate nohighlight">\(X\)</span>, such that <span class="math notranslate nohighlight">\(f(x)=y\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">Surjective</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">)</span> <span class="o">:</span> <span class="kt">Prop</span> <span class="o">:=</span> <span class="bp">&#8704;</span> <span class="n">y</span> <span class="o">:</span> <span class="n">Y</span><span class="o">,</span> <span class="bp">&#8707;</span> <span class="n">x</span> <span class="o">:</span> <span class="n">X</span><span class="o">,</span> <span class="n">f</span> <span class="n">x</span> <span class="bp">=</span> <span class="n">y</span>
</pre></div>
</div>
</section>
<section id="id5">
<h3><span class="section-number">8.1.6. </span>Example<a class="headerlink" href="#id5" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Consider the function <span class="math notranslate nohighlight">\(s:\mathbb{Q}\to\mathbb{Q}\)</span> defined by, <span class="math notranslate nohighlight">\(s(a)=3a+2\)</span>. Show that
<span class="math notranslate nohighlight">\(s\)</span> is surjective.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Let <span class="math notranslate nohighlight">\(y\)</span> be a rational number.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}s\left(\frac{y-2}{3}\right)&amp;=3\left(\frac{y-2}{3}\right)+2\\
&amp;=y.\end{split}\]</div>
</div>
<p>Here is the solution in Lean.  The goal state after unfolding the definition of &#8220;surjective&#8221; is</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>&#8866; &#8704; (y : &#8474;), &#8707; x, s x = y
</pre></div>
</div>
<p>which confirms what we need to prove and why what we wrote in the text proof above is sufficient.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">s</span> <span class="o">(</span><span class="n">a</span> <span class="o">:</span> <span class="n">&#8474;</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8474;</span> <span class="o">:=</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">+</span> <span class="mi">2</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Surjective</span> <span class="n">s</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Surjective</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">y</span>
  <span class="n">use</span> <span class="o">(</span><span class="n">y</span> <span class="bp">-</span> <span class="mi">2</span><span class="o">)</span> <span class="bp">/</span> <span class="mi">3</span>
  <span class="k">calc</span> <span class="n">s</span> <span class="o">((</span><span class="n">y</span> <span class="bp">-</span> <span class="mi">2</span><span class="o">)</span> <span class="bp">/</span> <span class="mi">3</span><span class="o">)</span> <span class="bp">=</span> <span class="mi">3</span> <span class="bp">*</span> <span class="o">((</span><span class="n">y</span> <span class="bp">-</span> <span class="mi">2</span><span class="o">)</span> <span class="bp">/</span> <span class="mi">3</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">s</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="n">y</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
</pre></div>
</div>
</section>
<section id="not-surjective">
<span id="id6"></span><h3><span class="section-number">8.1.7. </span>Example<a class="headerlink" href="#not-surjective" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that the function <span class="math notranslate nohighlight">\(x \mapsto x ^ 2\)</span> from <span class="math notranslate nohighlight">\(\mathbb{R}\)</span> to <span class="math notranslate nohighlight">\(\mathbb{R}\)</span>
is not surjective.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We will show that there exists a real number <span class="math notranslate nohighlight">\(y\)</span>, such that for all real numbers <span class="math notranslate nohighlight">\(x\)</span>,
<span class="math notranslate nohighlight">\(x^2\ne y\)</span>.</p>
<p>Indeed, let us show that -1 has this property.  Let <span class="math notranslate nohighlight">\(x\)</span> be a real number.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}-1&amp;&lt;0\\
&amp;\le x^2,\end{split}\]</div>
<p>so <span class="math notranslate nohighlight">\(x^2\ne -1\)</span>.</p>
</div>
<p>As in <a class="reference internal" href="#not-injective-example"><span class="std std-numref">Example 8.1.4</span></a>, the first sentence constitutes a
negation-normalization of the definition of &#8220;surjective&#8221; in this context.  Effectively we are stating
what would be the goal state in the Lean proof after <code class="docutils literal notranslate"><span class="pre">push_neg</span></code>.</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>&#8866; &#8707; y, &#8704; (x : &#8477;), x ^ 2 &#8800; y
</pre></div>
</div>
<p>And here is the full Lean proof.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Surjective</span> <span class="o">(</span><span class="k">fun</span> <span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">&#8614;</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Surjective</span><span class="o">]</span>
  <span class="n">push_neg</span>
  <span class="n">use</span> <span class="bp">-</span><span class="mi">1</span>
  <span class="n">intro</span> <span class="n">x</span>
  <span class="n">apply</span> <span class="n">ne_of_gt</span>
  <span class="k">calc</span> <span class="bp">-</span><span class="mi">1</span> <span class="bp">&lt;</span> <span class="mi">0</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">numbers</span>
    <span class="n">_</span> <span class="bp">&#8804;</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">extra</span>
</pre></div>
</div>
</section>
<section id="musketeer">
<span id="id7"></span><h3><span class="section-number">8.1.8. </span>Example<a class="headerlink" href="#musketeer" title="Permalink to this headline">&#61633;</a></h3>
<p>We have so far seen numeric types, like the integers <span class="math notranslate nohighlight">\(\mathbb{Z}\)</span> and the real numbers
<span class="math notranslate nohighlight">\(\mathbb{R}\)</span>, and function types, like <span class="math notranslate nohighlight">\(\mathbb{Z}\to \mathbb{R}\)</span> (the functions from
<span class="math notranslate nohighlight">\(\mathbb{Z}\)</span> to <span class="math notranslate nohighlight">\(\mathbb{R}\)</span>).</p>
<p>Another way to make a type is as a finite set of options.  Finite types are useful for conceptual
examples, because everything is explicit and checkable.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">inductive</span> <span class="n">Musketeer</span>
  <span class="bp">|</span> <span class="n">athos</span>
  <span class="bp">|</span> <span class="n">porthos</span>
  <span class="bp">|</span> <span class="n">aramis</span>
  <span class="n">deriving</span> <span class="n">DecidableEq</span>
</pre></div>
</div>
<p>Here is how to define a function whose domain is a given finite inductive type.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">f</span> <span class="o">:</span> <span class="n">Musketeer</span> <span class="bp">&#8594;</span> <span class="n">Musketeer</span>
  <span class="bp">|</span> <span class="n">athos</span> <span class="bp">=&gt;</span> <span class="n">aramis</span>
  <span class="bp">|</span> <span class="n">porthos</span> <span class="bp">=&gt;</span> <span class="n">aramis</span>
  <span class="bp">|</span> <span class="n">aramis</span> <span class="bp">=&gt;</span> <span class="n">athos</span>
</pre></div>
</div>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that the function <span class="math notranslate nohighlight">\(f\)</span> is not injective.</p>
</div>
<figure class="align-default">
<img alt="_images/musketeer1a.png" src="_images/musketeer1a.png" />
</figure>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Injective</span> <span class="n">f</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Injective</span><span class="o">]</span>
  <span class="n">push_neg</span>
  <span class="n">use</span> <span class="n">athos</span><span class="o">,</span> <span class="n">porthos</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">f</span><span class="o">]</span> <span class="c1">-- optional</span>
  <span class="n">exhaust</span>
</pre></div>
</div>
<p>The tactic <code class="docutils literal notranslate"><span class="pre">exhaust</span></code> is new here.  At the place where it is used, the goal state is</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>aramis = aramis &#8743; athos &#8800; porthos
</pre></div>
</div>
<p>that is,</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>True &#8743; &#172; False
</pre></div>
</div>
<p>which is logically equivalent to <code class="docutils literal notranslate"><span class="pre">True</span></code>.  The tactic <code class="docutils literal notranslate"><span class="pre">exhaust</span></code> can do this kind of propositional
logic reasoning, up to arbitrary complexity.</p>
<p>In particular, <code class="docutils literal notranslate"><span class="pre">exhaust</span></code> can prove any (true) variable-free statement in an inductive type, and
that&#8217;s how we&#8217;ll use it in this chapter.  We start making more serious use of <code class="docutils literal notranslate"><span class="pre">exhaust</span></code> in
<a class="reference internal" href="09_Sets.html#sets"><span class="std std-numref">Chapter 9</span></a>.</p>
</section>
<section id="id8">
<h3><span class="section-number">8.1.9. </span>Example<a class="headerlink" href="#id8" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that the function <span class="math notranslate nohighlight">\(f\)</span> defined in <a class="reference internal" href="#musketeer"><span class="std std-numref">Example 8.1.8</span></a> is not surjective.</p>
</div>
<figure class="align-default">
<img alt="_images/musketeer1b.png" src="_images/musketeer1b.png" />
</figure>
<p>We can case-check on a variable <code class="docutils literal notranslate"><span class="pre">a</span></code> in a finite inductive type using the tactic <code class="docutils literal notranslate"><span class="pre">cases</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Surjective</span> <span class="n">f</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Surjective</span><span class="o">]</span>
  <span class="n">push_neg</span>
  <span class="n">use</span> <span class="n">porthos</span>
  <span class="n">intro</span> <span class="n">a</span>
  <span class="n">cases</span> <span class="n">a</span>
  <span class="bp">&#183;</span> <span class="n">exhaust</span>
  <span class="bp">&#183;</span> <span class="n">exhaust</span>
  <span class="bp">&#183;</span> <span class="n">exhaust</span>
</pre></div>
</div>
<p>Such proofs can become repetitive, and you may wish to use a trick we have seen before (for example
<a class="reference internal" href="04_Proofs_with_Structure_II.html#prime-test"><span class="std std-numref">Example 4.4.4</span></a>, <a class="reference internal" href="04_Proofs_with_Structure_II.html#better-prime-test"><span class="std std-numref">Example 4.5.9</span></a>,
<a class="reference internal" href="06_Induction.html#mod-add-div"><span class="std std-numref">Example 6.6.2</span></a>, <a class="reference internal" href="06_Induction.html#gcd-nonneg"><span class="std std-numref">Example 6.7.2</span></a>): when a tactic such as
<code class="docutils literal notranslate"><span class="pre">cases</span></code> generates many goals which can all be proved by the same tactic, you can write
<code class="docutils literal notranslate"><span class="pre">&lt;;&gt;</span></code> to apply the tactic to all those goals.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="c1">-- better (more automated) version of the previous proof</span>
<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Surjective</span> <span class="n">f</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Surjective</span><span class="o">]</span>
  <span class="n">push_neg</span>
  <span class="n">use</span> <span class="n">porthos</span>
  <span class="n">intro</span> <span class="n">a</span>
  <span class="n">cases</span> <span class="n">a</span> <span class="bp">&lt;;&gt;</span> <span class="n">exhaust</span>
</pre></div>
</div>
<p>You might also like to check that the <code class="docutils literal notranslate"><span class="pre">cases</span> <span class="pre">a</span> <span class="pre">&lt;;&gt;</span> <span class="pre">exhaust</span></code> line is necessary; <code class="docutils literal notranslate"><span class="pre">exhaust</span></code> can&#8217;t close
the goal on its own.  As discussed in <a class="reference internal" href="#musketeer"><span class="std std-numref">Example 8.1.8</span></a>, <code class="docutils literal notranslate"><span class="pre">exhaust</span></code> can prove any
(true) <em>variable-free</em> statement in an inductive type, but before the <code class="docutils literal notranslate"><span class="pre">cases</span> <span class="pre">a</span> <span class="pre">&lt;;&gt;</span> <span class="pre">exhaust</span></code> line the
goal state is</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>a : Musketeer
&#8866; f a &#8800; porthos
</pre></div>
</div>
<p>which contains a variable, <code class="docutils literal notranslate"><span class="pre">a</span></code>.</p>
</section>
<section id="musketeer2">
<span id="id9"></span><h3><span class="section-number">8.1.10. </span>Example<a class="headerlink" href="#musketeer2" title="Permalink to this headline">&#61633;</a></h3>
<p>Let <span class="math notranslate nohighlight">\(g\)</span> be the following function from the Musketeer type to itself:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">g</span> <span class="o">:</span> <span class="n">Musketeer</span> <span class="bp">&#8594;</span> <span class="n">Musketeer</span>
  <span class="bp">|</span> <span class="n">athos</span> <span class="bp">=&gt;</span> <span class="n">porthos</span>
  <span class="bp">|</span> <span class="n">porthos</span> <span class="bp">=&gt;</span> <span class="n">aramis</span>
  <span class="bp">|</span> <span class="n">aramis</span> <span class="bp">=&gt;</span> <span class="n">athos</span>
</pre></div>
</div>
<figure class="align-default">
<img alt="_images/musketeer2.png" src="_images/musketeer2.png" />
</figure>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that the function <span class="math notranslate nohighlight">\(g\)</span> is injective.</p>
</div>
<p>There are a lot of cases in this proof &#8211; <span class="math notranslate nohighlight">\(3 \times 3 = 9\)</span>, to be precise.  Fortunately
<code class="docutils literal notranslate"><span class="pre">exhaust</span></code> can prove all of them!</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Injective</span> <span class="n">g</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Injective</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">x1</span> <span class="n">x2</span> <span class="n">hx</span>
  <span class="n">cases</span> <span class="n">x1</span> <span class="bp">&lt;;&gt;</span> <span class="n">cases</span> <span class="n">x2</span> <span class="bp">&lt;;&gt;</span> <span class="n">exhaust</span>
</pre></div>
</div>
</section>
<section id="id10">
<h3><span class="section-number">8.1.11. </span>Example<a class="headerlink" href="#id10" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that the function <span class="math notranslate nohighlight">\(g\)</span> defined in <a class="reference internal" href="#musketeer2"><span class="std std-numref">Example 8.1.10</span></a> is surjective.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Surjective</span> <span class="n">g</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Surjective</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">y</span>
  <span class="n">cases</span> <span class="n">y</span>
  <span class="bp">&#183;</span> <span class="n">use</span> <span class="n">aramis</span>
    <span class="n">exhaust</span>
  <span class="bp">&#183;</span> <span class="n">use</span> <span class="n">athos</span>
    <span class="n">exhaust</span>
  <span class="bp">&#183;</span> <span class="n">use</span> <span class="n">porthos</span>
    <span class="n">exhaust</span>
</pre></div>
</div>
</section>
<section id="id11">
<h3><span class="section-number">8.1.12. </span>Example<a class="headerlink" href="#id11" title="Permalink to this headline">&#61633;</a></h3>
<p>We finish with a relatively hard example.  The proof here is efficient and self-contained but not
particularly well-motivated.  For an alternative (perhaps more intuitive) approach, combine the last
exercise in this section (the one about <em>strictly monotone</em> functions) with the idea from
<a class="reference internal" href="02_Proofs_with_Structure.html#cube-inequality"><span class="std std-numref">Example 2.1.8</span></a>.</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that the function <span class="math notranslate nohighlight">\(x \mapsto x ^ 3\)</span> from <span class="math notranslate nohighlight">\(\mathbb{R}\)</span> to <span class="math notranslate nohighlight">\(\mathbb{R}\)</span> is
injective.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Let <span class="math notranslate nohighlight">\(x_1\)</span> and <span class="math notranslate nohighlight">\(x_2\)</span> be real numbers and suppose that <span class="math notranslate nohighlight">\(x_1{}^3=x_2{}^3\)</span>.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}(x_1-x_2)(x_1{}^2+x_1x_2+x_2{}^2)&amp;=x_1{}^3-x_2{}^3\\
  &amp;=x_1{}^3-x_1{}^3\\
  &amp;=0,\end{split}\]</div>
<p>so either <span class="math notranslate nohighlight">\(x_1-x_2=0\)</span>, in which case we are done, or <span class="math notranslate nohighlight">\(x_1{}^2+x_1x_2+x_2{}^2=0\)</span>, which
we henceforth assume.</p>
<p>We now consider a further case split according to whether <span class="math notranslate nohighlight">\(x_1=0\)</span>.</p>
<p><strong>Case 1</strong> (<span class="math notranslate nohighlight">\(x_1=0\)</span>): Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}x_2{}^3&amp;=x_1{}^3\\
  &amp;=0^3\\&amp;=0,\end{split}\]</div>
<p>so <span class="math notranslate nohighlight">\(x_2=0\)</span> also.  Thus <span class="math notranslate nohighlight">\(x_1=0=x_2\)</span> as required.</p>
<p><strong>Case 2</strong> (<span class="math notranslate nohighlight">\(x_1\ne 0\)</span>): Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}0&amp;&lt; x_1{}^2+\left((x_1+x_2)^2+x_2{}^2\right)\\
&amp;=2(x_1{}^2+x_1x_2+x_2{}^2)\\
&amp;=2\cdot 0\\
&amp;=0,\end{split}\]</div>
<p>contradiction.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Injective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">(</span><span class="n">x</span><span class="o">:</span><span class="n">&#8477;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">3</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">intro</span> <span class="n">x1</span> <span class="n">x2</span> <span class="n">hx</span>
  <span class="n">dsimp</span> <span class="n">at</span> <span class="n">hx</span>
  <span class="k">have</span> <span class="n">H</span> <span class="o">:</span> <span class="o">(</span><span class="n">x1</span> <span class="bp">-</span> <span class="n">x2</span><span class="o">)</span> <span class="bp">*</span> <span class="o">(</span><span class="n">x1</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="n">x1</span> <span class="bp">*</span> <span class="n">x2</span> <span class="bp">+</span> <span class="n">x2</span> <span class="bp">^</span> <span class="mi">2</span><span class="o">)</span> <span class="bp">=</span> <span class="mi">0</span>
  <span class="bp">&#183;</span> <span class="k">calc</span> <span class="o">(</span><span class="n">x1</span> <span class="bp">-</span> <span class="n">x2</span><span class="o">)</span> <span class="bp">*</span> <span class="o">(</span><span class="n">x1</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="n">x1</span> <span class="bp">*</span> <span class="n">x2</span> <span class="bp">+</span> <span class="n">x2</span> <span class="bp">^</span> <span class="mi">2</span><span class="o">)</span> <span class="bp">=</span> <span class="n">x1</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">-</span> <span class="n">x2</span> <span class="bp">^</span> <span class="mi">3</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="n">x1</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">-</span> <span class="n">x1</span> <span class="bp">^</span> <span class="mi">3</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hx</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="mi">0</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
  <span class="n">rw</span> <span class="o">[</span><span class="n">mul_eq_zero</span><span class="o">]</span> <span class="n">at</span> <span class="n">H</span>
  <span class="n">obtain</span> <span class="n">H1</span> <span class="bp">|</span> <span class="n">H2</span> <span class="o">:=</span> <span class="n">H</span>
  <span class="bp">&#183;</span> <span class="c1">-- case 1: x1 - x2 = 0</span>
    <span class="n">addarith</span> <span class="o">[</span><span class="n">H1</span><span class="o">]</span>
  <span class="bp">&#183;</span> <span class="c1">-- case 2: x1 ^2 + x1 * x2 + x2 ^ 2  = 0</span>
    <span class="n">by_cases</span> <span class="n">hx1</span> <span class="o">:</span> <span class="n">x1</span> <span class="bp">=</span> <span class="mi">0</span>
    <span class="bp">&#183;</span> <span class="c1">-- case 2a: x1 = 0</span>
      <span class="k">have</span> <span class="n">hx2</span> <span class="o">:=</span>
      <span class="k">calc</span> <span class="n">x2</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">=</span> <span class="n">x1</span> <span class="bp">^</span> <span class="mi">3</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hx</span><span class="o">]</span>
        <span class="n">_</span> <span class="bp">=</span> <span class="mi">0</span> <span class="bp">^</span> <span class="mi">3</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hx1</span><span class="o">]</span>
        <span class="n">_</span> <span class="bp">=</span> <span class="mi">0</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">numbers</span>
      <span class="n">cancel</span> <span class="mi">3</span> <span class="n">at</span> <span class="n">hx2</span>
      <span class="k">calc</span> <span class="n">x1</span> <span class="bp">=</span> <span class="mi">0</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hx1</span><span class="o">]</span>
        <span class="n">_</span> <span class="bp">=</span> <span class="n">x2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hx2</span><span class="o">]</span>
    <span class="bp">&#183;</span> <span class="c1">-- case 2b: x1 &#8800; 0</span>
      <span class="k">have</span> <span class="o">:=</span>
      <span class="k">calc</span> <span class="mi">0</span> <span class="bp">&lt;</span> <span class="n">x1</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="o">((</span><span class="n">x1</span> <span class="bp">+</span> <span class="n">x2</span><span class="o">)</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="n">x2</span> <span class="bp">^</span> <span class="mi">2</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">extra</span>
          <span class="n">_</span> <span class="bp">=</span> <span class="mi">2</span> <span class="bp">*</span> <span class="o">(</span><span class="n">x1</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="n">x1</span> <span class="bp">*</span> <span class="n">x2</span> <span class="bp">+</span> <span class="n">x2</span> <span class="bp">^</span> <span class="mi">2</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
          <span class="n">_</span> <span class="bp">=</span> <span class="mi">2</span> <span class="bp">*</span> <span class="mi">0</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">H2</span><span class="o">]</span>
          <span class="n">_</span> <span class="bp">=</span> <span class="mi">0</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
      <span class="n">numbers</span> <span class="n">at</span> <span class="n">this</span> <span class="c1">-- contradiction!</span>
</pre></div>
</div>
</section>
<section id="exercises">
<h3><span class="section-number">8.1.13. </span>Exercises<a class="headerlink" href="#exercises" title="Permalink to this headline">&#61633;</a></h3>
<ol class="arabic">
<li><p>Prove or disprove that the function <span class="math notranslate nohighlight">\(x \mapsto x-12\)</span> from <span class="math notranslate nohighlight">\(\mathbb{Q}\)</span> to
<span class="math notranslate nohighlight">\(\mathbb{Q}\)</span> is injective.</p>
<p>(If you think it&#8217;s true, prove it, by solving the first version below.  If you think it&#8217;s false,
solve the second version.)</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Injective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8474;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="n">x</span> <span class="bp">-</span> <span class="mi">12</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Injective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8474;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="n">x</span> <span class="bp">-</span> <span class="mi">12</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove or disprove that the function <span class="math notranslate nohighlight">\(x \mapsto 3\)</span> from <span class="math notranslate nohighlight">\(\mathbb{R}\)</span> to
<span class="math notranslate nohighlight">\(\mathbb{R}\)</span> is injective.</p>
<p>(If you think it&#8217;s true, prove it, by solving the first version below.  If you think it&#8217;s false,
solve the second version.)</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Injective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="mi">3</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Injective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="mi">3</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove or disprove that the function <span class="math notranslate nohighlight">\(x \mapsto 3x-1\)</span> from <span class="math notranslate nohighlight">\(\mathbb{&#8474;}\)</span> to
<span class="math notranslate nohighlight">\(\mathbb{&#8474;}\)</span> is injective.</p>
<p>(If you think it&#8217;s true, prove it, by solving the first version below.  If you think it&#8217;s false,
solve the second version.)</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Injective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8474;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">x</span> <span class="bp">-</span> <span class="mi">1</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Injective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8474;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">x</span> <span class="bp">-</span> <span class="mi">1</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove or disprove that the function <span class="math notranslate nohighlight">\(x \mapsto 3x-1\)</span> from <span class="math notranslate nohighlight">\(\mathbb{Z}\)</span> to
<span class="math notranslate nohighlight">\(\mathbb{Z}\)</span> is injective.</p>
<p>(If you think it&#8217;s true, prove it, by solving the first version below.  If you think it&#8217;s false,
solve the second version.)</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Injective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">x</span> <span class="bp">-</span> <span class="mi">1</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Injective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">x</span> <span class="bp">-</span> <span class="mi">1</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove or disprove that the function <span class="math notranslate nohighlight">\(x \mapsto 2x\)</span> from <span class="math notranslate nohighlight">\(\mathbb{R}\)</span> to
<span class="math notranslate nohighlight">\(\mathbb{R}\)</span> is surjective.</p>
<p>(If you think it&#8217;s true, prove it, by solving the first version below.  If you think it&#8217;s false,
solve the second version.)</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Surjective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">x</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Surjective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">x</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove or disprove that the function <span class="math notranslate nohighlight">\(x \mapsto 2x\)</span> from <span class="math notranslate nohighlight">\(\mathbb{Z}\)</span> to
<span class="math notranslate nohighlight">\(\mathbb{Z}\)</span> is surjective.</p>
<p>(If you think it&#8217;s true, prove it, by solving the first version below.  If you think it&#8217;s false,
solve the second version.)</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Surjective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">x</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Surjective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">x</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove or disprove that the function <span class="math notranslate nohighlight">\(n \mapsto n^2\)</span> from <span class="math notranslate nohighlight">\(\mathbb{N}\)</span> to
<span class="math notranslate nohighlight">\(\mathbb{N}\)</span> is surjective.</p>
<p>(If you think it&#8217;s true, prove it, by solving the first version below.  If you think it&#8217;s false,
solve the second version.)</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Surjective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Surjective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">(</span><span class="n">n</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Consider the following finite inductive type White, and the following function <span class="math notranslate nohighlight">\(h\)</span> from
the Musketeer type (see <a class="reference internal" href="#musketeer"><span class="std std-numref">Example 8.1.8</span></a>) to the White type. Prove or disprove
that the function <span class="math notranslate nohighlight">\(h\)</span> is injective.</p>
<p>(If you think it&#8217;s true, prove it, by solving the first version below.  If you think it&#8217;s false,
solve the second version.)</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">inductive</span> <span class="n">White</span>
  <span class="bp">|</span> <span class="n">meg</span>
  <span class="bp">|</span> <span class="n">jack</span>
  <span class="n">deriving</span> <span class="n">DecidableEq</span>

<span class="kn">open</span> <span class="n">White</span>

<span class="kd">def</span> <span class="n">h</span> <span class="o">:</span> <span class="n">Musketeer</span> <span class="bp">&#8594;</span> <span class="n">White</span>
  <span class="bp">|</span> <span class="n">athos</span> <span class="bp">=&gt;</span> <span class="n">jack</span>
  <span class="bp">|</span> <span class="n">porthos</span> <span class="bp">=&gt;</span> <span class="n">meg</span>
  <span class="bp">|</span> <span class="n">aramis</span> <span class="bp">=&gt;</span> <span class="n">jack</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Injective</span> <span class="n">h</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Injective</span> <span class="n">h</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove or disprove that the function <span class="math notranslate nohighlight">\(h\)</span> from the previous example is surjective.</p>
<p>(If you think it&#8217;s true, prove it, by solving the first version below.  If you think it&#8217;s false,
solve the second version.)</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Surjective</span> <span class="n">h</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Surjective</span> <span class="n">h</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Consider the following function <span class="math notranslate nohighlight">\(l\)</span> from the White type (see the previous two problems)
to the Musketeer type (see <a class="reference internal" href="#musketeer"><span class="std std-numref">Example 8.1.8</span></a>). Prove or
disprove that the function <span class="math notranslate nohighlight">\(l\)</span> is injective.</p>
<p>(If you think it&#8217;s true, prove it, by solving the first version below.  If you think it&#8217;s false,
solve the second version.)</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">l</span> <span class="o">:</span> <span class="n">White</span> <span class="bp">&#8594;</span> <span class="n">Musketeer</span>
  <span class="bp">|</span> <span class="n">meg</span> <span class="bp">=&gt;</span> <span class="n">aramis</span>
  <span class="bp">|</span> <span class="n">jack</span> <span class="bp">=&gt;</span> <span class="n">porthos</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Injective</span> <span class="n">l</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Injective</span> <span class="n">l</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove or disprove that the function <span class="math notranslate nohighlight">\(l\)</span> from the previous example is surjective.</p>
<p>(If you think it&#8217;s true, prove it, by solving the first version below.  If you think it&#8217;s false,
solve the second version.)</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Surjective</span> <span class="n">l</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Surjective</span> <span class="n">l</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(f : X \to Y\)</span> be a function.  Show that <span class="math notranslate nohighlight">\(f\)</span> is injective if and only if for all
<span class="math notranslate nohighlight">\(x_1\)</span> and <span class="math notranslate nohighlight">\(x_2\)</span> of type <span class="math notranslate nohighlight">\(X\)</span>, if <span class="math notranslate nohighlight">\(x_1\ne x_2\)</span>  then
<span class="math notranslate nohighlight">\(f(x_1)\ne f(x_2)\)</span>.</p>
<p>You will need to use a tactic (such as <code class="docutils literal notranslate"><span class="pre">push_neg</span></code> or <code class="docutils literal notranslate"><span class="pre">by_cases</span></code>) which is capable of
handling the subtler negations.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">)</span> <span class="o">:</span> <span class="n">Injective</span> <span class="n">f</span> <span class="bp">&#8596;</span> <span class="bp">&#8704;</span> <span class="n">x1</span> <span class="n">x2</span> <span class="o">:</span> <span class="n">X</span><span class="o">,</span> <span class="n">x1</span> <span class="bp">&#8800;</span> <span class="n">x2</span> <span class="bp">&#8594;</span> <span class="n">f</span> <span class="n">x1</span> <span class="bp">&#8800;</span> <span class="n">f</span> <span class="n">x2</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove or disprove that for all functions <span class="math notranslate nohighlight">\(f:\mathbb{Q}\to \mathbb{Q}\)</span>, if <span class="math notranslate nohighlight">\(f\)</span> is
injective, then the function <span class="math notranslate nohighlight">\(x \mapsto f(x)+1\)</span> from <span class="math notranslate nohighlight">\(\mathbb{Q}\)</span> to
<span class="math notranslate nohighlight">\(\mathbb{Q}\)</span> is also injective.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">&#8474;</span> <span class="bp">&#8594;</span> <span class="n">&#8474;</span><span class="o">),</span> <span class="n">Injective</span> <span class="n">f</span> <span class="bp">&#8594;</span> <span class="n">Injective</span> <span class="o">(</span><span class="k">fun</span> <span class="n">x</span> <span class="bp">&#8614;</span> <span class="n">f</span> <span class="n">x</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="bp">&#8704;</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">&#8474;</span> <span class="bp">&#8594;</span> <span class="n">&#8474;</span><span class="o">),</span> <span class="n">Injective</span> <span class="n">f</span> <span class="bp">&#8594;</span> <span class="n">Injective</span> <span class="o">(</span><span class="k">fun</span> <span class="n">x</span> <span class="bp">&#8614;</span> <span class="n">f</span> <span class="n">x</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove or disprove that for all functions <span class="math notranslate nohighlight">\(f:\mathbb{Q}\to \mathbb{Q}\)</span>, if <span class="math notranslate nohighlight">\(f\)</span> is
injective, then the function <span class="math notranslate nohighlight">\(x \mapsto f(x)+x\)</span> from <span class="math notranslate nohighlight">\(\mathbb{Q}\)</span> to
<span class="math notranslate nohighlight">\(\mathbb{Q}\)</span> is also injective.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">&#8474;</span> <span class="bp">&#8594;</span> <span class="n">&#8474;</span><span class="o">),</span> <span class="n">Injective</span> <span class="n">f</span> <span class="bp">&#8594;</span> <span class="n">Injective</span> <span class="o">(</span><span class="k">fun</span> <span class="n">x</span> <span class="bp">&#8614;</span> <span class="n">f</span> <span class="n">x</span> <span class="bp">+</span> <span class="n">x</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="bp">&#8704;</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">&#8474;</span> <span class="bp">&#8594;</span> <span class="n">&#8474;</span><span class="o">),</span> <span class="n">Injective</span> <span class="n">f</span> <span class="bp">&#8594;</span> <span class="n">Injective</span> <span class="o">(</span><span class="k">fun</span> <span class="n">x</span> <span class="bp">&#8614;</span> <span class="n">f</span> <span class="n">x</span> <span class="bp">+</span> <span class="n">x</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove or disprove that for all functions <span class="math notranslate nohighlight">\(f:\mathbb{Z}\to \mathbb{Z}\)</span>, if <span class="math notranslate nohighlight">\(f\)</span> is
surjective, then the function <span class="math notranslate nohighlight">\(x \mapsto 2f(x)\)</span> from <span class="math notranslate nohighlight">\(\mathbb{Z}\)</span> to
<span class="math notranslate nohighlight">\(\mathbb{Z}\)</span> is also surjective.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">&#8594;</span> <span class="n">&#8484;</span><span class="o">),</span> <span class="n">Surjective</span> <span class="n">f</span> <span class="bp">&#8594;</span> <span class="n">Surjective</span> <span class="o">(</span><span class="k">fun</span> <span class="n">x</span> <span class="bp">&#8614;</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">f</span> <span class="n">x</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="bp">&#8704;</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">&#8594;</span> <span class="n">&#8484;</span><span class="o">),</span> <span class="n">Surjective</span> <span class="n">f</span> <span class="bp">&#8594;</span> <span class="n">Surjective</span> <span class="o">(</span><span class="k">fun</span> <span class="n">x</span> <span class="bp">&#8614;</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">f</span> <span class="n">x</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove or disprove that for all real numbers <span class="math notranslate nohighlight">\(c\)</span>, the function <span class="math notranslate nohighlight">\(x\mapsto cx\)</span> from
<span class="math notranslate nohighlight">\(\mathbb{R}\)</span> to <span class="math notranslate nohighlight">\(\mathbb{R}\)</span> is surjective.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">c</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">,</span> <span class="n">Surjective</span> <span class="o">(</span><span class="k">fun</span> <span class="n">x</span> <span class="bp">&#8614;</span> <span class="n">c</span> <span class="bp">*</span> <span class="n">x</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="bp">&#8704;</span> <span class="n">c</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">,</span> <span class="n">Surjective</span> <span class="o">(</span><span class="k">fun</span> <span class="n">x</span> <span class="bp">&#8614;</span> <span class="n">c</span> <span class="bp">*</span> <span class="n">x</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(f:\mathbb{Q}\to\mathbb{Q}\)</span> be a function which is <em>strictly monotone</em>; that is, for
all real numbers <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> with <span class="math notranslate nohighlight">\(x&lt;y\)</span>, it is true that <span class="math notranslate nohighlight">\(f(x)&lt;f(y)\)</span>.
Prove that <span class="math notranslate nohighlight">\(f\)</span> is injective.</p>
<p>You may wish to use the lemma <code class="docutils literal notranslate"><span class="pre">lt_trichotomy</span></code></p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">lemma</span> <span class="n">lt_trichotomy</span> <span class="o">(</span><span class="n">x</span> <span class="n">y</span> <span class="o">:</span> <span class="n">&#8474;</span><span class="o">)</span> <span class="o">:</span> <span class="n">x</span> <span class="bp">&lt;</span> <span class="n">y</span> <span class="bp">&#8744;</span> <span class="n">x</span> <span class="bp">=</span> <span class="n">y</span> <span class="bp">&#8744;</span> <span class="n">x</span> <span class="bp">&lt;</span> <span class="n">y</span> <span class="o">:=</span>
</pre></div>
</div>
<p>which gives a case division on the relative sizes of two real numbers.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">&#8474;</span> <span class="bp">&#8594;</span> <span class="n">&#8474;</span><span class="o">}</span> <span class="o">(</span><span class="n">hf</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">x</span> <span class="n">y</span><span class="o">,</span> <span class="n">x</span> <span class="bp">&lt;</span> <span class="n">y</span> <span class="bp">&#8594;</span> <span class="n">f</span> <span class="n">x</span> <span class="bp">&lt;</span> <span class="n">f</span> <span class="n">y</span><span class="o">)</span> <span class="o">:</span> <span class="n">Injective</span> <span class="n">f</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(f:X\to\mathbb{N}\)</span> be a function, let <span class="math notranslate nohighlight">\(x_0\)</span> be of type <span class="math notranslate nohighlight">\(X\)</span> with
<span class="math notranslate nohighlight">\(f(x_0)=0\)</span>, and let <span class="math notranslate nohighlight">\(i:X\to X\)</span> be a function such that, for all <span class="math notranslate nohighlight">\(x\)</span>,
<span class="math notranslate nohighlight">\(f(i(x))=f(x)+1\)</span>.  Show that <span class="math notranslate nohighlight">\(f\)</span> is surjective.  I recommend induction.</p>
<p>We record this theorem for future use under the name <code class="docutils literal notranslate"><span class="pre">surjective_of_intertwining</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">&#8469;</span><span class="o">}</span> <span class="o">{</span><span class="n">x0</span> <span class="o">:</span> <span class="n">X</span><span class="o">}</span> <span class="o">(</span><span class="n">h0</span> <span class="o">:</span> <span class="n">f</span> <span class="n">x0</span> <span class="bp">=</span> <span class="mi">0</span><span class="o">)</span> <span class="o">{</span><span class="n">i</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">X</span><span class="o">}</span>
    <span class="o">(</span><span class="n">hi</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">x</span><span class="o">,</span> <span class="n">f</span> <span class="o">(</span><span class="n">i</span> <span class="n">x</span><span class="o">)</span> <span class="bp">=</span> <span class="n">f</span> <span class="n">x</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="o">:</span> <span class="n">Surjective</span> <span class="n">f</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
</ol>
</section>
</section>
<section id="bijectivity">
<span id="bij"></span><h2><span class="section-number">8.2. </span>Bijectivity<a class="headerlink" href="#bijectivity" title="Permalink to this headline">&#61633;</a></h2>
<section id="id12">
<h3><span class="section-number">8.2.1. </span>Definition<a class="headerlink" href="#id12" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-definition admonition">
<p class="admonition-title">Definition</p>
<p>A function is <em>bijective</em>, if it is both injective and surjective.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">Bijective</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">)</span> <span class="o">:</span> <span class="kt">Prop</span> <span class="o">:=</span> <span class="n">Injective</span> <span class="n">f</span> <span class="bp">&#8743;</span> <span class="n">Surjective</span> <span class="n">f</span>
</pre></div>
</div>
</section>
<section id="id13">
<h3><span class="section-number">8.2.2. </span>Example<a class="headerlink" href="#id13" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(p:\mathbb{R}\to\mathbb{R}\)</span> be the function defined by, <span class="math notranslate nohighlight">\(p(x)=2x-5\)</span>.
Show that <span class="math notranslate nohighlight">\(p\)</span> is bijective.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We must show that <span class="math notranslate nohighlight">\(p\)</span> is injective and surjective.</p>
<p>For the injectivity, let <span class="math notranslate nohighlight">\(x_1\)</span> and <span class="math notranslate nohighlight">\(x_2\)</span> be real numbers and suppose that
<span class="math notranslate nohighlight">\(p(x_1)=p(x_2)\)</span>.  This means that <span class="math notranslate nohighlight">\(2x_1-5=2x_2-5\)</span>.  So</p>
<div class="math notranslate nohighlight">
\[\begin{split}x_1&amp;= \frac{(2x_1-5)+5}{2}\\
&amp;= \frac{(2x_2-5)+5}{2}\\
&amp;=x_2.\end{split}\]</div>
<p>For the surjectivity, let <span class="math notranslate nohighlight">\(y\)</span> be a real number.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}p \left(\frac{y+5}{2}\right)&amp;=2\left(\frac{y+5}{2}\right)-5\\
&amp;=y.\end{split}\]</div>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">p</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="o">:=</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">x</span> <span class="bp">-</span> <span class="mi">5</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Bijective</span> <span class="n">p</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Bijective</span><span class="o">]</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">dsimp</span> <span class="o">[</span><span class="n">Injective</span><span class="o">]</span>
    <span class="n">intro</span> <span class="n">x1</span> <span class="n">x2</span> <span class="n">hx</span>
    <span class="n">dsimp</span> <span class="o">[</span><span class="n">p</span><span class="o">]</span> <span class="n">at</span> <span class="n">hx</span>
    <span class="k">calc</span> <span class="n">x1</span> <span class="bp">=</span> <span class="o">((</span><span class="mi">2</span> <span class="bp">*</span> <span class="n">x1</span> <span class="bp">-</span> <span class="mi">5</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">5</span><span class="o">)</span> <span class="bp">/</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="o">((</span><span class="mi">2</span> <span class="bp">*</span> <span class="n">x2</span> <span class="bp">-</span> <span class="mi">5</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">5</span><span class="o">)</span> <span class="bp">/</span> <span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hx</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="n">x2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
  <span class="bp">&#183;</span> <span class="n">dsimp</span> <span class="o">[</span><span class="n">Surjective</span><span class="o">]</span>
    <span class="n">intro</span> <span class="n">y</span>
    <span class="n">use</span> <span class="o">(</span><span class="n">y</span> <span class="bp">+</span> <span class="mi">5</span><span class="o">)</span> <span class="bp">/</span> <span class="mi">2</span>
    <span class="k">calc</span> <span class="n">p</span> <span class="o">((</span><span class="n">y</span> <span class="bp">+</span> <span class="mi">5</span><span class="o">)</span> <span class="bp">/</span> <span class="mi">2</span><span class="o">)</span> <span class="bp">=</span> <span class="mi">2</span> <span class="bp">*</span> <span class="o">((</span><span class="n">y</span> <span class="bp">+</span> <span class="mi">5</span><span class="o">)</span> <span class="bp">/</span> <span class="mi">2</span><span class="o">)</span> <span class="bp">-</span> <span class="mi">5</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rfl</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="n">y</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
</pre></div>
</div>
</section>
<section id="id14">
<h3><span class="section-number">8.2.3. </span>Example<a class="headerlink" href="#id14" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(a:\mathbb{R}\to\mathbb{R}\)</span> be the function defined by, <span class="math notranslate nohighlight">\(a(t)=t^3-t\)</span>.
Show that <span class="math notranslate nohighlight">\(a\)</span> is not bijective.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We will show that <span class="math notranslate nohighlight">\(a\)</span> is not injective.  Indeed, note that <span class="math notranslate nohighlight">\(0\ne 1\)</span> but</p>
<div class="math notranslate nohighlight">
\[\begin{split}a(0)&amp;=0^3-0\\
  &amp;=1^3-1\\
  &amp;=a(1).\end{split}\]</div>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">a</span> <span class="o">(</span><span class="n">t</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="o">:=</span> <span class="n">t</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">-</span> <span class="n">t</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Bijective</span> <span class="n">a</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Bijective</span><span class="o">]</span>
  <span class="n">push_neg</span>
  <span class="n">left</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Injective</span><span class="o">]</span>
  <span class="n">push_neg</span>
  <span class="n">use</span> <span class="mi">0</span><span class="o">,</span> <span class="mi">1</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="k">calc</span> <span class="n">a</span> <span class="mi">0</span> <span class="bp">=</span> <span class="mi">0</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">-</span> <span class="mi">0</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rfl</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="mi">1</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">-</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">numbers</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="n">a</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rfl</span>
  <span class="bp">&#183;</span> <span class="n">numbers</span>
</pre></div>
</div>
</section>
<section id="celestial-subatomic">
<span id="id15"></span><h3><span class="section-number">8.2.4. </span>Example<a class="headerlink" href="#celestial-subatomic" title="Permalink to this headline">&#61633;</a></h3>
<p>Consider the following finite inductive types Celestial and Subatomic:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">inductive</span> <span class="n">Celestial</span>
  <span class="bp">|</span> <span class="n">sun</span>
  <span class="bp">|</span> <span class="n">moon</span>
  <span class="n">deriving</span> <span class="n">DecidableEq</span>

<span class="kd">inductive</span> <span class="n">Subatomic</span>
  <span class="bp">|</span> <span class="n">proton</span>
  <span class="bp">|</span> <span class="n">neutron</span>
  <span class="bp">|</span> <span class="n">electron</span>
  <span class="n">deriving</span> <span class="n">DecidableEq</span>
</pre></div>
</div>
<p>Consider the following function <span class="math notranslate nohighlight">\(f\)</span> from the Celestial type to the Subatomic type.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">f</span> <span class="o">:</span> <span class="n">Celestial</span> <span class="bp">&#8594;</span> <span class="n">Subatomic</span>
  <span class="bp">|</span> <span class="n">sun</span> <span class="bp">=&gt;</span> <span class="n">proton</span>
  <span class="bp">|</span> <span class="n">moon</span> <span class="bp">=&gt;</span> <span class="n">electron</span>
</pre></div>
</div>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Prove that the function <span class="math notranslate nohighlight">\(f\)</span> is not bijective.</p>
</div>
<figure class="align-default">
<img alt="_images/celestial_subatomic.png" src="_images/celestial_subatomic.png" />
</figure>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Bijective</span> <span class="n">f</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Bijective</span><span class="o">]</span>
  <span class="n">push_neg</span>
  <span class="n">right</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Surjective</span><span class="o">]</span>
  <span class="n">push_neg</span>
  <span class="n">use</span> <span class="n">neutron</span>
  <span class="n">intro</span> <span class="n">x</span>
  <span class="n">cases</span> <span class="n">x</span> <span class="bp">&lt;;&gt;</span> <span class="n">exhaust</span>
</pre></div>
</div>
</section>
<section id="id16">
<h3><span class="section-number">8.2.5. </span>Example<a class="headerlink" href="#id16" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-theorem admonition">
<p class="admonition-title">Theorem</p>
<p>A function <span class="math notranslate nohighlight">\(f:X\to Y\)</span> is bijective, if and only if for all <span class="math notranslate nohighlight">\(y\)</span> of type <span class="math notranslate nohighlight">\(Y\)</span>,
there exists a unique <span class="math notranslate nohighlight">\(x\)</span> of type <span class="math notranslate nohighlight">\(X\)</span>, such that <span class="math notranslate nohighlight">\(f(x)=y\)</span>.</p>
</div>
<div class="admonition-proof admonition">
<p class="admonition-title">Proof</p>
<p>First, suppose that <span class="math notranslate nohighlight">\(f\)</span> is bijective. Let <span class="math notranslate nohighlight">\(y\)</span> be of type <span class="math notranslate nohighlight">\(Y\)</span>.  Since <span class="math notranslate nohighlight">\(f\)</span>
is surjective, there exists <span class="math notranslate nohighlight">\(x\)</span> of type <span class="math notranslate nohighlight">\(X\)</span>, such that <span class="math notranslate nohighlight">\(f(x)=y\)</span>. We will show
that this <span class="math notranslate nohighlight">\(x\)</span> is unique.  Indeed, for any other <span class="math notranslate nohighlight">\(x'\)</span> with <span class="math notranslate nohighlight">\(f(x')=y\)</span>, we have
that</p>
<div class="math notranslate nohighlight">
\[\begin{split}f(x')&amp;=y\\
&amp;=f(x),\end{split}\]</div>
<p>and so by the injectivity of <span class="math notranslate nohighlight">\(f\)</span>, <span class="math notranslate nohighlight">\(x'=x\)</span>.</p>
<p>Conversely, suppose that  for all <span class="math notranslate nohighlight">\(y\)</span> of type <span class="math notranslate nohighlight">\(Y\)</span>, there exists a unique <span class="math notranslate nohighlight">\(x\)</span> of
type <span class="math notranslate nohighlight">\(X\)</span>, such that <span class="math notranslate nohighlight">\(f(x)=y\)</span>.  (<span class="math notranslate nohighlight">\(\star\)</span>) We must show that <span class="math notranslate nohighlight">\(f\)</span> is
injective and surjective.</p>
<p>For the injectivity, let <span class="math notranslate nohighlight">\(x_1\)</span> and <span class="math notranslate nohighlight">\(x_2\)</span> be of type <span class="math notranslate nohighlight">\(X\)</span>, and suppose that
<span class="math notranslate nohighlight">\(f(x_1)=f(x_2)\)</span>.   By  (<span class="math notranslate nohighlight">\(\star\)</span>) applied with <span class="math notranslate nohighlight">\(y=f(x_1)\)</span>, there exists a unique
<span class="math notranslate nohighlight">\(x\)</span> of type <span class="math notranslate nohighlight">\(X\)</span> for which <span class="math notranslate nohighlight">\(f(x)=f(x_1)\)</span>.  So, by the uniqueness, <span class="math notranslate nohighlight">\(x_1=x\)</span>,
and also, since <span class="math notranslate nohighlight">\(f(x_2)=f(x_1)=f(x)\)</span>, <span class="math notranslate nohighlight">\(x_2=x\)</span>.  Combining these, <span class="math notranslate nohighlight">\(x_1=x_2\)</span>.</p>
<p>For the surjectivity, let <span class="math notranslate nohighlight">\(y\)</span> be of type <span class="math notranslate nohighlight">\(Y\)</span>.  By  (<span class="math notranslate nohighlight">\(\star\)</span>), there exists (a
unique) <span class="math notranslate nohighlight">\(x\)</span> of type <span class="math notranslate nohighlight">\(X\)</span> for which <span class="math notranslate nohighlight">\(f(x)=y\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">}</span> <span class="o">:</span> <span class="n">Bijective</span> <span class="n">f</span> <span class="bp">&#8596;</span> <span class="bp">&#8704;</span> <span class="n">y</span><span class="o">,</span> <span class="bp">&#8707;!</span> <span class="n">x</span><span class="o">,</span> <span class="n">f</span> <span class="n">x</span> <span class="bp">=</span> <span class="n">y</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="c1">-- if `f` is bijective then `&#8704; y, &#8707;! x, f x = y`</span>
    <span class="n">intro</span> <span class="n">h</span> <span class="n">y</span>
    <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">h_inj</span><span class="o">,</span> <span class="n">h_surj</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h</span>
    <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">x</span><span class="o">,</span> <span class="n">hx</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h_surj</span> <span class="n">y</span>
    <span class="n">use</span> <span class="n">x</span>
    <span class="n">dsimp</span>
    <span class="n">constructor</span>
    <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">hx</span>
    <span class="bp">&#183;</span> <span class="n">intro</span> <span class="n">x&#39;</span> <span class="n">hx&#39;</span>
      <span class="n">apply</span> <span class="n">h_inj</span>
      <span class="k">calc</span> <span class="n">f</span> <span class="n">x&#39;</span> <span class="bp">=</span> <span class="n">y</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hx&#39;</span><span class="o">]</span>
        <span class="n">_</span> <span class="bp">=</span> <span class="n">f</span> <span class="n">x</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hx</span><span class="o">]</span>
  <span class="bp">&#183;</span> <span class="c1">-- if `&#8704; y, &#8707;! x, f x = y` then `f` is bijective</span>
    <span class="n">intro</span> <span class="n">h</span>
    <span class="n">constructor</span>
    <span class="bp">&#183;</span> <span class="c1">-- `f` is injective</span>
      <span class="n">intro</span> <span class="n">x1</span> <span class="n">x2</span> <span class="n">hx1x2</span>
      <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">x</span><span class="o">,</span> <span class="n">hx</span><span class="o">,</span> <span class="n">hx&#39;</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h</span> <span class="o">(</span><span class="n">f</span> <span class="n">x1</span><span class="o">)</span>
      <span class="k">have</span> <span class="n">hxx1</span> <span class="o">:</span> <span class="n">x1</span> <span class="bp">=</span> <span class="n">x</span>
      <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">hx&#39;</span>
        <span class="n">rfl</span>
      <span class="k">have</span> <span class="n">hxx2</span> <span class="o">:</span> <span class="n">x2</span> <span class="bp">=</span> <span class="n">x</span>
      <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">hx&#39;</span>
        <span class="n">rw</span> <span class="o">[</span><span class="n">hx1x2</span><span class="o">]</span>
      <span class="k">calc</span> <span class="n">x1</span> <span class="bp">=</span> <span class="n">x</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hxx1</span><span class="o">]</span>
        <span class="n">_</span> <span class="bp">=</span> <span class="n">x2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hxx2</span><span class="o">]</span>
    <span class="bp">&#183;</span> <span class="c1">-- `f` is surjective</span>
      <span class="n">intro</span> <span class="n">y</span>
      <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">x</span><span class="o">,</span> <span class="n">hx</span><span class="o">,</span> <span class="n">hx&#39;</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h</span> <span class="n">y</span>
      <span class="n">use</span> <span class="n">x</span>
      <span class="n">apply</span> <span class="n">hx</span>
</pre></div>
</div>
</section>
<section id="bij-card2">
<span id="id17"></span><h3><span class="section-number">8.2.6. </span>Example<a class="headerlink" href="#bij-card2" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that for all functions <span class="math notranslate nohighlight">\(f\)</span> from the Celestial type
(<a class="reference internal" href="#celestial-subatomic"><span class="std std-numref">Example 8.2.4</span></a>) to itself, if <span class="math notranslate nohighlight">\(f\)</span> is injective then it is
bijective.</p>
</div>
<p>We prove this by an exhaustive analysis of all functions <span class="math notranslate nohighlight">\(f\)</span> from the Celestial type to
itself.  There are four such functions.  I dealt with the first two cases below; fill in the second
two cases yourself.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">f</span> <span class="o">:</span> <span class="n">Celestial</span> <span class="bp">&#8594;</span> <span class="n">Celestial</span><span class="o">,</span> <span class="n">Injective</span> <span class="n">f</span> <span class="bp">&#8594;</span> <span class="n">Bijective</span> <span class="n">f</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">intro</span> <span class="n">f</span> <span class="n">hf</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="c1">-- `f` is injective by assumption</span>
    <span class="n">apply</span> <span class="n">hf</span>
  <span class="c1">-- show that `f` is surjective</span>
  <span class="k">match</span> <span class="n">h_sun</span> <span class="o">:</span> <span class="n">f</span> <span class="n">sun</span><span class="o">,</span> <span class="n">h_moon</span> <span class="o">:</span> <span class="n">f</span> <span class="n">moon</span> <span class="k">with</span>
  <span class="bp">|</span> <span class="n">sun</span><span class="o">,</span> <span class="n">sun</span> <span class="bp">=&gt;</span>
    <span class="k">have</span> <span class="o">:</span> <span class="n">sun</span> <span class="bp">=</span> <span class="n">moon</span>
    <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">hf</span>
      <span class="n">rw</span> <span class="o">[</span><span class="n">h_sun</span><span class="o">,</span> <span class="n">h_moon</span><span class="o">]</span>
    <span class="n">contradiction</span>
  <span class="bp">|</span> <span class="n">sun</span><span class="o">,</span> <span class="n">moon</span> <span class="bp">=&gt;</span>
    <span class="n">intro</span> <span class="n">y</span>
    <span class="n">cases</span> <span class="n">y</span>
    <span class="bp">&#183;</span> <span class="n">use</span> <span class="n">sun</span>
      <span class="n">apply</span> <span class="n">h_sun</span>
    <span class="bp">&#183;</span> <span class="n">use</span> <span class="n">moon</span>
      <span class="n">apply</span> <span class="n">h_moon</span>
  <span class="bp">|</span> <span class="n">moon</span><span class="o">,</span> <span class="n">sun</span> <span class="bp">=&gt;</span> <span class="gr">sorry</span>
  <span class="bp">|</span> <span class="n">moon</span><span class="o">,</span> <span class="n">moon</span> <span class="bp">=&gt;</span> <span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="id18">
<h3><span class="section-number">8.2.7. </span>Example<a class="headerlink" href="#id18" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Show that it is not true that for all functions <span class="math notranslate nohighlight">\(f:\mathbb{N}\to \mathbb{N}\)</span>, if <span class="math notranslate nohighlight">\(f\)</span>
is injective then it is bijective.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We must show that there exists a function <span class="math notranslate nohighlight">\(f:\mathbb{N}\to \mathbb{N}\)</span>, which is injective
but not bijective.</p>
<p>Indeed, consider the function <span class="math notranslate nohighlight">\(f(n)=n+1\)</span>.  This function is injective, since for all
natural numbers <span class="math notranslate nohighlight">\(n_1\)</span> and <span class="math notranslate nohighlight">\(n_2\)</span>, if <span class="math notranslate nohighlight">\(n_1+1=n_2+1\)</span> then <span class="math notranslate nohighlight">\(n_1=n_2\)</span>.</p>
<p>However, this function is not surjective, and therefore not bijective.  To see this, observe that
for all natural numbers <span class="math notranslate nohighlight">\(n\)</span>, we have <span class="math notranslate nohighlight">\(f(n)=n+1&gt;0\)</span> and therefore <span class="math notranslate nohighlight">\(f(n)\ne 0\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="bp">&#8704;</span> <span class="n">f</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">&#8469;</span><span class="o">,</span> <span class="n">Injective</span> <span class="n">f</span> <span class="bp">&#8594;</span> <span class="n">Bijective</span> <span class="n">f</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">push_neg</span>
  <span class="n">use</span> <span class="k">fun</span> <span class="n">n</span> <span class="bp">&#8614;</span> <span class="n">n</span> <span class="bp">+</span> <span class="mi">1</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="c1">-- the function is injective</span>
    <span class="n">intro</span> <span class="n">n1</span> <span class="n">n2</span> <span class="n">hn</span>
    <span class="n">addarith</span> <span class="o">[</span><span class="n">hn</span><span class="o">]</span>
  <span class="bp">&#183;</span> <span class="c1">-- the function is not bijective</span>
    <span class="n">dsimp</span> <span class="o">[</span><span class="n">Bijective</span><span class="o">]</span>
    <span class="n">push_neg</span>
    <span class="n">right</span>
    <span class="c1">-- specifically, it&#39;s not surjective</span>
    <span class="n">dsimp</span> <span class="o">[</span><span class="n">Surjective</span><span class="o">]</span>
    <span class="n">push_neg</span>
    <span class="n">use</span> <span class="mi">0</span>
    <span class="n">intro</span> <span class="n">n</span>
    <span class="n">apply</span> <span class="n">ne_of_gt</span>
    <span class="n">extra</span>
</pre></div>
</div>
</section>
<section id="id19">
<h3><span class="section-number">8.2.8. </span>Exercises<a class="headerlink" href="#id19" title="Permalink to this headline">&#61633;</a></h3>
<ol class="arabic">
<li><p>Prove or disprove that the function <span class="math notranslate nohighlight">\(x \mapsto 4-3x\)</span> from <span class="math notranslate nohighlight">\(\mathbb{R}\)</span> to
<span class="math notranslate nohighlight">\(\mathbb{R}\)</span> is bijective.</p>
<p>(If you think it&#8217;s true, prove it, by solving the first version below.  If you think it&#8217;s false,
solve the second version.)</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Bijective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="mi">4</span> <span class="bp">-</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">x</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Bijective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="mi">4</span> <span class="bp">-</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">x</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Prove or disprove that the function <span class="math notranslate nohighlight">\(x \mapsto x^2+2x\)</span> from <span class="math notranslate nohighlight">\(\mathbb{R}\)</span> to
<span class="math notranslate nohighlight">\(\mathbb{R}\)</span> is bijective.</p>
<p>(If you think it&#8217;s true, prove it, by solving the first version below.  If you think it&#8217;s false,
solve the second version.)</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Bijective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">x</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Bijective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">x</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Consider the following finite inductive type Element, and the following function <span class="math notranslate nohighlight">\(e\)</span> from
the Element type to itself. Prove or disprove that the function <span class="math notranslate nohighlight">\(e\)</span> is bijective.</p>
<p>(If you think it&#8217;s true, prove it, by solving the first version below.  If you think it&#8217;s false,
solve the second version.)</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">inductive</span> <span class="n">Element</span>
  <span class="bp">|</span> <span class="n">fire</span>
  <span class="bp">|</span> <span class="n">water</span>
  <span class="bp">|</span> <span class="n">earth</span>
  <span class="bp">|</span> <span class="n">air</span>
  <span class="n">deriving</span> <span class="n">DecidableEq</span>

<span class="kn">open</span> <span class="n">Element</span>

<span class="kd">def</span> <span class="n">e</span> <span class="o">:</span> <span class="n">Element</span> <span class="bp">&#8594;</span> <span class="n">Element</span>
  <span class="bp">|</span> <span class="n">fire</span> <span class="bp">=&gt;</span> <span class="n">earth</span>
  <span class="bp">|</span> <span class="n">water</span> <span class="bp">=&gt;</span> <span class="n">air</span>
  <span class="bp">|</span> <span class="n">earth</span> <span class="bp">=&gt;</span> <span class="n">fire</span>
  <span class="bp">|</span> <span class="n">air</span> <span class="bp">=&gt;</span> <span class="n">water</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Bijective</span> <span class="n">e</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Bijective</span> <span class="n">e</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Show that for all functions <span class="math notranslate nohighlight">\(f\)</span> from the Subatomic type
(<a class="reference internal" href="#celestial-subatomic"><span class="std std-numref">Example 8.2.4</span></a>) to itself, if <span class="math notranslate nohighlight">\(f\)</span> is injective then it is
bijective.</p>
<p>This is like <a class="reference internal" href="#bij-card2"><span class="std std-numref">Example 8.2.6</span></a>, but with more cases to check.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">f</span> <span class="o">:</span> <span class="n">Subatomic</span> <span class="bp">&#8594;</span> <span class="n">Subatomic</span><span class="o">,</span> <span class="n">Injective</span> <span class="n">f</span> <span class="bp">&#8594;</span> <span class="n">Bijective</span> <span class="n">f</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Consider the finite inductive type Element from a previous exercise.  Show that for all
functions <span class="math notranslate nohighlight">\(f\)</span> from the Element type to itself, if <span class="math notranslate nohighlight">\(f\)</span> is injective then it is
bijective.</p>
<p>This is like <a class="reference internal" href="#bij-card2"><span class="std std-numref">Example 8.2.6</span></a> and the previous exercise, but with even more
(frankly, way too many &#8230;.) cases to check.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#8704;</span> <span class="n">f</span> <span class="o">:</span> <span class="n">Element</span> <span class="bp">&#8594;</span> <span class="n">Element</span><span class="o">,</span> <span class="n">Injective</span> <span class="n">f</span> <span class="bp">&#8594;</span> <span class="n">Bijective</span> <span class="n">f</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
</ol>
</section>
</section>
<section id="composition-of-functions">
<span id="composition"></span><h2><span class="section-number">8.3. </span>Composition of functions<a class="headerlink" href="#composition-of-functions" title="Permalink to this headline">&#61633;</a></h2>
<section id="id20">
<h3><span class="section-number">8.3.1. </span>Definition<a class="headerlink" href="#id20" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-definition admonition">
<p class="admonition-title">Definition</p>
<p>The <em>composition</em> of the function <span class="math notranslate nohighlight">\(g : Y \to Z\)</span> with the function <span class="math notranslate nohighlight">\(f : X \to Y\)</span> is the
function from <span class="math notranslate nohighlight">\(X\)</span> to <span class="math notranslate nohighlight">\(Z\)</span> which sends <span class="math notranslate nohighlight">\(x\)</span> to <span class="math notranslate nohighlight">\(g(f(x))\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">comp</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">)</span> <span class="o">(</span><span class="n">g</span> <span class="o">:</span> <span class="n">Y</span> <span class="bp">&#8594;</span> <span class="n">Z</span><span class="o">)</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">X</span><span class="o">)</span> <span class="o">:</span> <span class="n">Z</span> <span class="o">:=</span> <span class="n">g</span> <span class="o">(</span><span class="n">f</span> <span class="n">x</span><span class="o">)</span>
</pre></div>
</div>
<p>The composition of <span class="math notranslate nohighlight">\(g : Y \to Z\)</span> with <span class="math notranslate nohighlight">\(f : X \to Y\)</span> is denoted <span class="math notranslate nohighlight">\(g \circ f\)</span> (in
Lean, <code class="docutils literal notranslate"><span class="pre">g</span> <span class="pre">&#8728;</span> <span class="pre">f</span></code>).</p>
</section>
<section id="ext">
<span id="id21"></span><h3><span class="section-number">8.3.2. </span>Example<a class="headerlink" href="#ext" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(f:\mathbb{R}\to\mathbb{R}\)</span> be the function defined by, <span class="math notranslate nohighlight">\(f(a)=a+3\)</span>.
Let <span class="math notranslate nohighlight">\(g:\mathbb{R}\to\mathbb{R}\)</span> be the function defined by, <span class="math notranslate nohighlight">\(g(b)=2b\)</span>.
Let <span class="math notranslate nohighlight">\(h:\mathbb{R}\to\mathbb{R}\)</span> be the function defined by, <span class="math notranslate nohighlight">\(h(c)=2c+6\)</span>.</p>
<p>Show that <span class="math notranslate nohighlight">\(g \circ f = h\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Let <span class="math notranslate nohighlight">\(x\)</span> be a real number.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}(g \circ f) (x)&amp;=g(f(x))\\
&amp;=2(x+3)\\
&amp;=2x+6\\
&amp;=h(x).\end{split}\]</div>
</div>
<p>In the Lean proof, note the new tactic <code class="docutils literal notranslate"><span class="pre">ext</span></code>.  To prove two functions are equal, we have to
show that they are equal on every input.  This is what the tactic <code class="docutils literal notranslate"><span class="pre">ext</span></code> does.  (The name stands
for &#8220;extensionality&#8221;.) Before we use it, the goal state is</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>&#8866; g &#8728; f = h
</pre></div>
</div>
<p>After we use it, the goal state is</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>x : &#8477;
&#8866; (g &#8728; f) x = h x
</pre></div>
</div>
<p>Here is the full Lean proof.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">f</span> <span class="o">(</span><span class="n">a</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="o">:=</span> <span class="n">a</span> <span class="bp">+</span> <span class="mi">3</span>
<span class="kd">def</span> <span class="n">g</span> <span class="o">(</span><span class="n">b</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="o">:=</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">b</span>
<span class="kd">def</span> <span class="n">h</span> <span class="o">(</span><span class="n">c</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="o">:=</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">c</span> <span class="bp">+</span> <span class="mi">6</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">g</span> <span class="bp">&#8728;</span> <span class="n">f</span> <span class="bp">=</span> <span class="n">h</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">ext</span> <span class="n">x</span>
  <span class="k">calc</span> <span class="o">(</span><span class="n">g</span> <span class="bp">&#8728;</span> <span class="n">f</span><span class="o">)</span> <span class="n">x</span> <span class="bp">=</span> <span class="n">g</span> <span class="o">(</span><span class="n">f</span> <span class="n">x</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rfl</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="mi">2</span> <span class="bp">*</span> <span class="o">(</span><span class="n">x</span> <span class="bp">+</span> <span class="mi">3</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rfl</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">x</span> <span class="bp">+</span> <span class="mi">6</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="n">h</span> <span class="n">x</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rfl</span>
</pre></div>
</div>
</section>
<section id="id22">
<h3><span class="section-number">8.3.3. </span>Definition<a class="headerlink" href="#id22" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-definition admonition">
<p class="admonition-title">Definition</p>
<p>The <em>identity function</em> <span class="math notranslate nohighlight">\(\operatorname{Id}_X:X\to X\)</span> is the function which sends each
<span class="math notranslate nohighlight">\(x\)</span> of type <span class="math notranslate nohighlight">\(X\)</span> to itself.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">id</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">X</span><span class="o">)</span> <span class="o">:</span> <span class="n">X</span> <span class="o">:=</span> <span class="n">x</span>
</pre></div>
</div>
</section>
<section id="id23">
<h3><span class="section-number">8.3.4. </span>Example<a class="headerlink" href="#id23" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Let <span class="math notranslate nohighlight">\(s:\mathbb{R}\to\mathbb{R}\)</span> be the function defined by, <span class="math notranslate nohighlight">\(s(x)=5-x\)</span>.</p>
<p>Show that <span class="math notranslate nohighlight">\(s \circ s = \operatorname{Id}_\mathbb{R}\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Let <span class="math notranslate nohighlight">\(x\)</span> be a real number.  We must show that <span class="math notranslate nohighlight">\(5 - (5 - x) = x\)</span>, which is true.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">s</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="o">:=</span> <span class="mi">5</span> <span class="bp">-</span> <span class="n">x</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">s</span> <span class="bp">&#8728;</span> <span class="n">s</span> <span class="bp">=</span> <span class="n">id</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">ext</span> <span class="n">x</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">s</span><span class="o">]</span>
  <span class="n">ring</span>
</pre></div>
</div>
</section>
<section id="id24">
<h3><span class="section-number">8.3.5. </span>Definition<a class="headerlink" href="#id24" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-definition admonition">
<p class="admonition-title">Definition</p>
<p>A function <span class="math notranslate nohighlight">\(g : Y \to X\)</span> is an <em>inverse</em> of <span class="math notranslate nohighlight">\(f : X \to Y\)</span>, if
<span class="math notranslate nohighlight">\(g \circ f=\operatorname{Id}_X\)</span> and <span class="math notranslate nohighlight">\(f \circ g=\operatorname{Id}_Y\)</span>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">Inverse</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">)</span> <span class="o">(</span><span class="n">g</span> <span class="o">:</span> <span class="n">Y</span> <span class="bp">&#8594;</span> <span class="n">X</span><span class="o">)</span> <span class="o">:</span> <span class="kt">Prop</span> <span class="o">:=</span> <span class="n">g</span> <span class="bp">&#8728;</span> <span class="n">f</span> <span class="bp">=</span> <span class="n">id</span> <span class="bp">&#8743;</span> <span class="n">f</span> <span class="bp">&#8728;</span> <span class="n">g</span> <span class="bp">=</span> <span class="n">id</span>
</pre></div>
</div>
</section>
<section id="humour">
<span id="id25"></span><h3><span class="section-number">8.3.6. </span>Example<a class="headerlink" href="#humour" title="Permalink to this headline">&#61633;</a></h3>
<p>Consider the following finite inductive type Humour:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">inductive</span> <span class="n">Humour</span>
  <span class="bp">|</span> <span class="n">melancholic</span>
  <span class="bp">|</span> <span class="n">choleric</span>
  <span class="bp">|</span> <span class="n">phlegmatic</span>
  <span class="bp">|</span> <span class="n">sanguine</span>
  <span class="n">deriving</span> <span class="n">DecidableEq</span>
</pre></div>
</div>
<p>Consider the following function <span class="math notranslate nohighlight">\(p\)</span> from the Humour type to itself.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">p</span> <span class="o">:</span> <span class="n">Humour</span> <span class="bp">&#8594;</span> <span class="n">Humour</span>
  <span class="bp">|</span> <span class="n">melancholic</span> <span class="bp">=&gt;</span> <span class="n">choleric</span>
  <span class="bp">|</span> <span class="n">choleric</span> <span class="bp">=&gt;</span> <span class="n">sanguine</span>
  <span class="bp">|</span> <span class="n">phlegmatic</span> <span class="bp">=&gt;</span> <span class="n">phlegmatic</span>
  <span class="bp">|</span> <span class="n">sanguine</span> <span class="bp">=&gt;</span> <span class="n">melancholic</span>
</pre></div>
</div>
<figure class="align-default">
<img alt="_images/humour.png" src="_images/humour.png" />
</figure>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Define a function <span class="math notranslate nohighlight">\(q\)</span> from the Humour type to itself which is inverse to <span class="math notranslate nohighlight">\(p\)</span>, and
prove this.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">q</span> <span class="o">:</span> <span class="n">Humour</span> <span class="bp">&#8594;</span> <span class="n">Humour</span>
  <span class="bp">|</span> <span class="n">melancholic</span> <span class="bp">=&gt;</span> <span class="n">sanguine</span>
  <span class="bp">|</span> <span class="n">choleric</span> <span class="bp">=&gt;</span> <span class="n">melancholic</span>
  <span class="bp">|</span> <span class="n">phlegmatic</span> <span class="bp">=&gt;</span> <span class="n">phlegmatic</span>
  <span class="bp">|</span> <span class="n">sanguine</span> <span class="bp">=&gt;</span> <span class="n">choleric</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Inverse</span> <span class="n">p</span> <span class="n">q</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">ext</span> <span class="n">x</span>
    <span class="n">cases</span> <span class="n">x</span> <span class="bp">&lt;;&gt;</span> <span class="n">exhaust</span>
  <span class="bp">&#183;</span> <span class="n">ext</span> <span class="n">x</span>
    <span class="n">cases</span> <span class="n">x</span> <span class="bp">&lt;;&gt;</span> <span class="n">exhaust</span>
</pre></div>
</div>
</section>
<section id="bijective-to-inverse">
<span id="id26"></span><h3><span class="section-number">8.3.7. </span>Example<a class="headerlink" href="#bijective-to-inverse" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-proposition admonition">
<p class="admonition-title">Proposition</p>
<p>Let <span class="math notranslate nohighlight">\(f : X \to Y\)</span> be a bijective function.  Then there exists a function
<span class="math notranslate nohighlight">\(g : Y \to X\)</span> which is inverse to <span class="math notranslate nohighlight">\(f\)</span>.</p>
</div>
<div class="admonition-proof admonition">
<p class="admonition-title">Proof</p>
<p>Define a function <span class="math notranslate nohighlight">\(g : Y \to X\)</span> as follows: given <span class="math notranslate nohighlight">\(y\)</span> of type <span class="math notranslate nohighlight">\(Y\)</span>, by the
surjectivity of <span class="math notranslate nohighlight">\(f\)</span> there exists an <span class="math notranslate nohighlight">\(x\)</span> of type <span class="math notranslate nohighlight">\(X\)</span> such that <span class="math notranslate nohighlight">\(f(x)=y\)</span>,
and we set <span class="math notranslate nohighlight">\(g(y)\)</span> to be this <span class="math notranslate nohighlight">\(x\)</span>.  Thus, for all <span class="math notranslate nohighlight">\(y\)</span>, it is true that
<span class="math notranslate nohighlight">\(f(g(y))=y\)</span>. (<span class="math notranslate nohighlight">\(\star\)</span>)</p>
<p>This immediately shows that <span class="math notranslate nohighlight">\(f \circ g = \operatorname{Id}_Y\)</span>.  To show that
<span class="math notranslate nohighlight">\(g \circ f = \operatorname{Id}_X\)</span>, let <span class="math notranslate nohighlight">\(x\)</span> be of type <span class="math notranslate nohighlight">\(X\)</span>.  We have, by
(<span class="math notranslate nohighlight">\(\star\)</span>), that</p>
<div class="math notranslate nohighlight">
\[\begin{split}f((g \circ f)(x))&amp;=f(g(f(x)))\\
&amp;=f(x)\\
&amp;=f(\operatorname{Id}_X(x)),\end{split}\]</div>
<p>so by the injectivity of <span class="math notranslate nohighlight">\(f\)</span>, it follows that
<span class="math notranslate nohighlight">\((g \circ f)(x) = \operatorname{Id}_X(x)\)</span>.</p>
</div>
<p>To write this proof in Lean, we need a tactic, <code class="docutils literal notranslate"><span class="pre">choose</span></code>, <a class="footnote-reference brackets" href="#id31" id="id27">1</a> which is not used elsewhere in the
book. This tactic constructs the function <span class="math notranslate nohighlight">\(g : Y \to X\)</span>
as described in the first paragraph of the text proof.  More precisely, given the hypothesis</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>h_surj: &#8704; (b : Y), &#8707; a, f a = b
</pre></div>
</div>
<p>the tactic invocation <code class="docutils literal notranslate"><span class="pre">choose</span> <span class="pre">g</span> <span class="pre">hg</span> <span class="pre">using</span> <span class="pre">h_surj</span></code> creates a function consisting of a &#8220;choice&#8221; of
the <code class="docutils literal notranslate"><span class="pre">a</span></code> for each <code class="docutils literal notranslate"><span class="pre">b</span></code>:</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>g : Y &#8594; X
hg : &#8704; (b : Y), f (g b) = b
</pre></div>
</div>
<p>Here is the full proof in Lean.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">exists_inverse_of_bijective</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">}</span> <span class="o">(</span><span class="n">hf</span> <span class="o">:</span> <span class="n">Bijective</span> <span class="n">f</span><span class="o">)</span> <span class="o">:</span>
    <span class="bp">&#8707;</span> <span class="n">g</span> <span class="o">:</span> <span class="n">Y</span> <span class="bp">&#8594;</span> <span class="n">X</span><span class="o">,</span> <span class="n">Inverse</span> <span class="n">f</span> <span class="n">g</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Bijective</span><span class="o">]</span> <span class="n">at</span> <span class="n">hf</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">h_inj</span><span class="o">,</span> <span class="n">h_surj</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">hf</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Surjective</span><span class="o">]</span> <span class="n">at</span> <span class="n">h_surj</span>
  <span class="n">choose</span> <span class="n">g</span> <span class="n">hg</span> <span class="n">using</span> <span class="n">h_surj</span>
  <span class="n">use</span> <span class="n">g</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Inverse</span><span class="o">]</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="c1">-- prove `g &#8728; f = id`</span>
    <span class="n">ext</span> <span class="n">x</span>
    <span class="n">dsimp</span> <span class="o">[</span><span class="n">Injective</span><span class="o">]</span> <span class="n">at</span> <span class="n">h_inj</span>
    <span class="n">apply</span> <span class="n">h_inj</span>
    <span class="k">calc</span> <span class="n">f</span> <span class="o">((</span><span class="n">g</span> <span class="bp">&#8728;</span> <span class="n">f</span><span class="o">)</span> <span class="n">x</span><span class="o">)</span> <span class="bp">=</span> <span class="n">f</span> <span class="o">(</span><span class="n">g</span> <span class="o">(</span><span class="n">f</span> <span class="n">x</span><span class="o">))</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rfl</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="n">f</span> <span class="n">x</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">apply</span> <span class="n">hg</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="n">f</span> <span class="o">(</span><span class="n">id</span> <span class="n">x</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rfl</span>
  <span class="bp">&#183;</span> <span class="c1">-- prove `f &#8728; g = id`</span>
    <span class="n">ext</span> <span class="n">y</span>
    <span class="n">apply</span> <span class="n">hg</span>
</pre></div>
</div>
</section>
<section id="inverse-to-bijection">
<span id="id28"></span><h3><span class="section-number">8.3.8. </span>Example<a class="headerlink" href="#inverse-to-bijection" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-proposition admonition">
<p class="admonition-title">Proposition</p>
<p>Let <span class="math notranslate nohighlight">\(f : X \to Y\)</span> and <span class="math notranslate nohighlight">\(g : Y \to X\)</span> be functions, with <span class="math notranslate nohighlight">\(g : Y \to X\)</span> inverse
to <span class="math notranslate nohighlight">\(f : X \to Y\)</span>.  Then <span class="math notranslate nohighlight">\(f : X \to Y\)</span> is bijective.</p>
</div>
<div class="admonition-proof admonition">
<p class="admonition-title">Proof</p>
<p>We first show <span class="math notranslate nohighlight">\(f\)</span> is injective.  Indeed, let <span class="math notranslate nohighlight">\(x_1\)</span> and <span class="math notranslate nohighlight">\(x_2\)</span> be of type
<span class="math notranslate nohighlight">\(X\)</span>, and suppose that  <span class="math notranslate nohighlight">\(f(x_1)=f(x_2)\)</span>.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}x_1&amp;=\operatorname{Id}_X(x_1)\\
&amp;=(g\circ f)(x_1)\\
&amp;=g(f(x_1))\\
&amp;=g(f(x_2))\\
&amp;=(g\circ f)(x_2)\\
&amp;=\operatorname{Id}_X(x_2)\\
&amp;=x_2.\end{split}\]</div>
<p>We now show that <span class="math notranslate nohighlight">\(f\)</span> is surjective.  Indeed, let <span class="math notranslate nohighlight">\(y\)</span> be of type <span class="math notranslate nohighlight">\(Y\)</span>.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}f(g(y))&amp;=(f\circ g)(y)\\
&amp;=\operatorname{Id}_Y(y)\\
&amp;=y.\end{split}\]</div>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">bijective_of_inverse</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">}</span> <span class="o">{</span><span class="n">g</span> <span class="o">:</span> <span class="n">Y</span> <span class="bp">&#8594;</span> <span class="n">X</span><span class="o">}</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">Inverse</span> <span class="n">f</span> <span class="n">g</span><span class="o">)</span> <span class="o">:</span>
    <span class="n">Bijective</span> <span class="n">f</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Inverse</span><span class="o">]</span> <span class="n">at</span> <span class="n">h</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">hgf</span><span class="o">,</span> <span class="n">hfg</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="c1">-- `f` is injective</span>
    <span class="n">intro</span> <span class="n">x1</span> <span class="n">x2</span> <span class="n">hx</span>
    <span class="k">calc</span> <span class="n">x1</span> <span class="bp">=</span> <span class="n">id</span> <span class="n">x1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rfl</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="o">(</span><span class="n">g</span> <span class="bp">&#8728;</span> <span class="n">f</span><span class="o">)</span> <span class="n">x1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hgf</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="n">g</span> <span class="o">(</span><span class="n">f</span> <span class="n">x1</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rfl</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="n">g</span> <span class="o">(</span><span class="n">f</span> <span class="n">x2</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hx</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="o">(</span><span class="n">g</span> <span class="bp">&#8728;</span> <span class="n">f</span><span class="o">)</span> <span class="n">x2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rfl</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="n">id</span> <span class="n">x2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hgf</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="n">x2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rfl</span>
  <span class="bp">&#183;</span> <span class="c1">-- `f` is surjective</span>
    <span class="n">intro</span> <span class="n">y</span>
    <span class="n">use</span> <span class="n">g</span> <span class="n">y</span>
    <span class="k">calc</span> <span class="n">f</span> <span class="o">(</span><span class="n">g</span> <span class="n">y</span><span class="o">)</span> <span class="bp">=</span> <span class="o">(</span><span class="n">f</span> <span class="bp">&#8728;</span> <span class="n">g</span><span class="o">)</span> <span class="n">y</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rfl</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="n">id</span> <span class="n">y</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">hfg</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="n">y</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rfl</span>
</pre></div>
</div>
</section>
<section id="bijective-iff-inverse">
<span id="id29"></span><h3><span class="section-number">8.3.9. </span>Example<a class="headerlink" href="#bijective-iff-inverse" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-theorem admonition">
<p class="admonition-title">Theorem</p>
<p>Let <span class="math notranslate nohighlight">\(f : X \to Y\)</span> be a function.  Then <span class="math notranslate nohighlight">\(f\)</span> is bijective, if and only if there
exists a function <span class="math notranslate nohighlight">\(g : Y \to X\)</span> which is inverse to <span class="math notranslate nohighlight">\(f\)</span>.</p>
</div>
<div class="admonition-proof admonition">
<p class="admonition-title">Proof</p>
<p>The first direction is given by <a class="reference internal" href="#bijective-to-inverse"><span class="std std-numref">Example 8.3.7</span></a>, and the second
direction by <a class="reference internal" href="#inverse-to-bijection"><span class="std std-numref">Example 8.3.8</span></a>.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">bijective_iff_exists_inverse</span> <span class="o">(</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">)</span> <span class="o">:</span>
    <span class="n">Bijective</span> <span class="n">f</span> <span class="bp">&#8596;</span> <span class="bp">&#8707;</span> <span class="n">g</span> <span class="o">:</span> <span class="n">Y</span> <span class="bp">&#8594;</span> <span class="n">X</span><span class="o">,</span> <span class="n">Inverse</span> <span class="n">f</span> <span class="n">g</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">exists_inverse_of_bijective</span>
  <span class="bp">&#183;</span> <span class="n">intro</span> <span class="n">h</span>
    <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">g</span><span class="o">,</span> <span class="n">H</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h</span>
    <span class="n">apply</span> <span class="n">bijective_of_inverse</span> <span class="n">H</span>
</pre></div>
</div>
</section>
<section id="id30">
<h3><span class="section-number">8.3.10. </span>Exercises<a class="headerlink" href="#id30" title="Permalink to this headline">&#61633;</a></h3>
<ol class="arabic">
<li><p>Consider the following functions <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b\)</span> from the Humour type (see
<a class="reference internal" href="#humour"><span class="std std-numref">Example 8.3.6</span></a>) to itself. Write down a function <span class="math notranslate nohighlight">\(c\)</span> from the Humour type
to itself, so that <span class="math notranslate nohighlight">\(b \circ a=c\)</span>.</p>
<p>When you have the right function written down, the included proof will work.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">a</span> <span class="o">:</span> <span class="n">Humour</span> <span class="bp">&#8594;</span> <span class="n">Humour</span>
  <span class="bp">|</span> <span class="n">melancholic</span> <span class="bp">=&gt;</span> <span class="n">sanguine</span>
  <span class="bp">|</span> <span class="n">choleric</span> <span class="bp">=&gt;</span> <span class="n">choleric</span>
  <span class="bp">|</span> <span class="n">phlegmatic</span> <span class="bp">=&gt;</span> <span class="n">phlegmatic</span>
  <span class="bp">|</span> <span class="n">sanguine</span> <span class="bp">=&gt;</span> <span class="n">melancholic</span>

<span class="kd">def</span> <span class="n">b</span> <span class="o">:</span> <span class="n">Humour</span> <span class="bp">&#8594;</span> <span class="n">Humour</span>
  <span class="bp">|</span> <span class="n">melancholic</span> <span class="bp">=&gt;</span> <span class="n">phlegmatic</span>
  <span class="bp">|</span> <span class="n">choleric</span> <span class="bp">=&gt;</span> <span class="n">phlegmatic</span>
  <span class="bp">|</span> <span class="n">phlegmatic</span> <span class="bp">=&gt;</span> <span class="n">melancholic</span>
  <span class="bp">|</span> <span class="n">sanguine</span> <span class="bp">=&gt;</span> <span class="n">sanguine</span>

<span class="kd">def</span> <span class="n">c</span> <span class="o">:</span> <span class="n">Humour</span> <span class="bp">&#8594;</span> <span class="n">Humour</span>
  <span class="bp">|</span> <span class="n">melancholic</span> <span class="bp">=&gt;</span> <span class="gr">sorry</span>
  <span class="bp">|</span> <span class="n">choleric</span> <span class="bp">=&gt;</span> <span class="gr">sorry</span>
  <span class="bp">|</span> <span class="n">phlegmatic</span> <span class="bp">=&gt;</span> <span class="gr">sorry</span>
  <span class="bp">|</span> <span class="n">sanguine</span> <span class="bp">=&gt;</span> <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">b</span> <span class="bp">&#8728;</span> <span class="n">a</span> <span class="bp">=</span> <span class="n">c</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">ext</span> <span class="n">x</span>
  <span class="n">cases</span> <span class="n">x</span> <span class="bp">&lt;;&gt;</span> <span class="n">exhaust</span>
</pre></div>
</div>
</li>
<li><p>Consider the function <span class="math notranslate nohighlight">\(u:\mathbb{R}\to\mathbb{R}\)</span> defined by, <span class="math notranslate nohighlight">\(u(x)=5x+1\)</span>. Write
down a function <span class="math notranslate nohighlight">\(v:\mathbb{R}\to\mathbb{R}\)</span> which is inverse to <span class="math notranslate nohighlight">\(u\)</span>, and prove it.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">u</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="o">:=</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">x</span> <span class="bp">+</span> <span class="mi">1</span>

<span class="kd">noncomputable</span> <span class="kd">def</span> <span class="n">v</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="o">:=</span> <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Inverse</span> <span class="n">u</span> <span class="n">v</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(f : X \to Y\)</span> and <span class="math notranslate nohighlight">\(g : Y \to Z\)</span> be injective functions.  Show that
<span class="math notranslate nohighlight">\(g \circ f\)</span> is also injective.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">}</span> <span class="o">(</span><span class="n">hf</span> <span class="o">:</span> <span class="n">Injective</span> <span class="n">f</span><span class="o">)</span> <span class="o">{</span><span class="n">g</span> <span class="o">:</span> <span class="n">Y</span> <span class="bp">&#8594;</span> <span class="n">Z</span><span class="o">}</span> <span class="o">(</span><span class="n">hg</span> <span class="o">:</span> <span class="n">Injective</span> <span class="n">g</span><span class="o">)</span> <span class="o">:</span>
    <span class="n">Injective</span> <span class="o">(</span><span class="n">g</span> <span class="bp">&#8728;</span> <span class="n">f</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(f : X \to Y\)</span> and <span class="math notranslate nohighlight">\(g : Y \to Z\)</span> be surjective functions.  Show that
<span class="math notranslate nohighlight">\(g \circ f\)</span> is also surjective.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">}</span> <span class="o">(</span><span class="n">hf</span> <span class="o">:</span> <span class="n">Surjective</span> <span class="n">f</span><span class="o">)</span> <span class="o">{</span><span class="n">g</span> <span class="o">:</span> <span class="n">Y</span> <span class="bp">&#8594;</span> <span class="n">Z</span><span class="o">}</span> <span class="o">(</span><span class="n">hg</span> <span class="o">:</span> <span class="n">Surjective</span> <span class="n">g</span><span class="o">)</span> <span class="o">:</span>
    <span class="n">Surjective</span> <span class="o">(</span><span class="n">g</span> <span class="bp">&#8728;</span> <span class="n">f</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(f : X \to Y\)</span> be a surjective function.  Show that there exists a function
<span class="math notranslate nohighlight">\(g : Y \to Z\)</span>, such that <span class="math notranslate nohighlight">\(f \circ g=\operatorname{Id}_Y\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">}</span> <span class="o">(</span><span class="n">hf</span> <span class="o">:</span> <span class="n">Surjective</span> <span class="n">f</span><span class="o">)</span> <span class="o">:</span> <span class="bp">&#8707;</span> <span class="n">g</span> <span class="o">:</span> <span class="n">Y</span> <span class="bp">&#8594;</span> <span class="n">X</span><span class="o">,</span> <span class="n">f</span> <span class="bp">&#8728;</span> <span class="n">g</span> <span class="bp">=</span> <span class="n">id</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(f : X \to Y\)</span> and <span class="math notranslate nohighlight">\(g : Y \to X\)</span> be functions, with <span class="math notranslate nohighlight">\(g\)</span> inverse
to <span class="math notranslate nohighlight">\(f\)</span>.  Show that <span class="math notranslate nohighlight">\(f\)</span> is inverse to <span class="math notranslate nohighlight">\(g\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">}</span> <span class="o">{</span><span class="n">g</span> <span class="o">:</span> <span class="n">Y</span> <span class="bp">&#8594;</span> <span class="n">X</span><span class="o">}</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">Inverse</span> <span class="n">f</span> <span class="n">g</span><span class="o">)</span> <span class="o">:</span> <span class="n">Inverse</span> <span class="n">g</span> <span class="n">f</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Let <span class="math notranslate nohighlight">\(f : X \to Y\)</span> and <span class="math notranslate nohighlight">\(g_1, g_2 : Y \to X\)</span> be functions, with both <span class="math notranslate nohighlight">\(g_1\)</span> and
<span class="math notranslate nohighlight">\(g_1\)</span> inverse to <span class="math notranslate nohighlight">\(f\)</span>.  Show that <span class="math notranslate nohighlight">\(g_1=g_2\)</span>.</p>
<p>This problem says that if a function <span class="math notranslate nohighlight">\(f\)</span> has an inverse, then that inverse is unique.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">f</span> <span class="o">:</span> <span class="n">X</span> <span class="bp">&#8594;</span> <span class="n">Y</span><span class="o">}</span> <span class="o">{</span><span class="n">g1</span> <span class="n">g2</span> <span class="o">:</span> <span class="n">Y</span> <span class="bp">&#8594;</span> <span class="n">X</span><span class="o">}</span> <span class="o">(</span><span class="n">h1</span> <span class="o">:</span> <span class="n">Inverse</span> <span class="n">f</span> <span class="n">g1</span><span class="o">)</span> <span class="o">(</span><span class="n">h2</span> <span class="o">:</span> <span class="n">Inverse</span> <span class="n">f</span> <span class="n">g2</span><span class="o">)</span> <span class="o">:</span>
    <span class="n">g1</span> <span class="bp">=</span> <span class="n">g2</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
</ol>
<p class="rubric">Footnotes</p>
<dl class="footnote brackets">
<dt class="label" id="id31"><span class="brackets"><a class="fn-backref" href="#id27">1</a></span></dt>
<dd><p>Experts will recognize this as the
<a class="reference external" href="https://en.wikipedia.org/wiki/Axiom_of_choice">axiom of choice</a>.</p>
</dd>
</dl>
</section>
</section>
<section id="product-types">
<span id="products"></span><h2><span class="section-number">8.4. </span>Product types<a class="headerlink" href="#product-types" title="Permalink to this headline">&#61633;</a></h2>
<section id="obtain-product">
<span id="id32"></span><h3><span class="section-number">8.4.1. </span>Example<a class="headerlink" href="#obtain-product" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Consider the function <span class="math notranslate nohighlight">\(q:\mathbb{Z}\to\mathbb{Z}^2\)</span> defined by, <span class="math notranslate nohighlight">\(q(m)=(m + 1, 2 - m)\)</span>.
Show that <span class="math notranslate nohighlight">\(q\)</span> is</p>
<ol class="arabic simple">
<li><p>injective;</p></li>
<li><p>not surjective.</p></li>
</ol>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<ol class="arabic">
<li><p>Let <span class="math notranslate nohighlight">\(m_1\)</span> and <span class="math notranslate nohighlight">\(m_2\)</span> be integers and suppose that <span class="math notranslate nohighlight">\(q(m_1)=q(m_2)\)</span>.  Then
by definition</p>
<div class="math notranslate nohighlight">
\[(m_1+1,2-m_1)=(m_2+1,2-m_2),\]</div>
<p>so <span class="math notranslate nohighlight">\(m_1+1=m_2+1\)</span> and <span class="math notranslate nohighlight">\(2-m_1=2-m_2\)</span>, so <span class="math notranslate nohighlight">\(m_1=m_2\)</span>.</p>
</li>
<li><p>We will show that there exists <span class="math notranslate nohighlight">\((a,b)\)</span> in <span class="math notranslate nohighlight">\(\mathbb{Z}^2\)</span> such that for all
integers <span class="math notranslate nohighlight">\(m\)</span>, <span class="math notranslate nohighlight">\(q(m)\ne(a,b)\)</span>.  Indeed, we will show that <span class="math notranslate nohighlight">\((0,1)\)</span> has this
property.  Suppose that <span class="math notranslate nohighlight">\(m\)</span> were an integer with <span class="math notranslate nohighlight">\(q(m)=(0,1)\)</span>.  Then by definition</p>
<div class="math notranslate nohighlight">
\[(m+1,2-m)=(0,1),\]</div>
<p>so <span class="math notranslate nohighlight">\(m+1=0\)</span> and <span class="math notranslate nohighlight">\(2-m=1\)</span>, hence</p>
<div class="math notranslate nohighlight">
\[\begin{split}1&amp;=(m+1)+(2-m)-2\\
&amp;=0+1-2\\
&amp;=-1,\end{split}\]</div>
<p>contradiction.</p>
</li>
</ol>
</div>
<p>To write these proofs in Lean, notice the use of the tactic <code class="docutils literal notranslate"><span class="pre">obtain</span></code> in the injectivity problem to
convert the hypothesis of a equality in a product type,</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>hm : (m1 + 1, 2 - m1) = (m2 + 1, 2 - m2)
</pre></div>
</div>
<p>to two hypotheses of equality in the two components of the product:</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>hm&#39; : m1 + 1 = m2 + 1
hm&#39;&#39; : 2 - m1 = 2 - m2
</pre></div>
</div>
<p>This is consistent with how you should think about equality in a product type: two ordered pairs are
equal if the two left parts are equal <em>and</em> the two right parts are equal.  So we use the same
tactic, with the same syntax, as for the logical operator &#8220;and&#8221;.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">q</span> <span class="o">(</span><span class="n">m</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">&#215;</span> <span class="n">&#8484;</span> <span class="o">:=</span> <span class="o">(</span><span class="n">m</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">,</span> <span class="mi">2</span> <span class="bp">-</span> <span class="n">m</span><span class="o">)</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Injective</span> <span class="n">q</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Injective</span><span class="o">]</span>
  <span class="n">intro</span> <span class="n">m1</span> <span class="n">m2</span> <span class="n">hm</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">q</span><span class="o">]</span> <span class="n">at</span> <span class="n">hm</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">hm&#39;</span><span class="o">,</span> <span class="n">hm&#39;&#39;</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">hm</span>
  <span class="n">addarith</span> <span class="o">[</span><span class="n">hm&#39;</span><span class="o">]</span>
</pre></div>
</div>
<p>The tactic <code class="docutils literal notranslate"><span class="pre">obtain</span></code> is used similarly in the non-surjectivity problem to break down the hypothesis
of equality in a product type</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>hm : (m + 1, 2 - m) = (0, 1)
</pre></div>
</div>
<p>which arises in that problem.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Surjective</span> <span class="n">q</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Surjective</span><span class="o">]</span>
  <span class="n">push_neg</span>
  <span class="n">use</span> <span class="o">(</span><span class="mi">0</span><span class="o">,</span> <span class="mi">1</span><span class="o">)</span>
  <span class="n">intro</span> <span class="n">m</span> <span class="n">hm</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">q</span><span class="o">]</span> <span class="n">at</span> <span class="n">hm</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">hm1</span><span class="o">,</span> <span class="n">hm2</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">hm</span>
  <span class="k">have</span> <span class="n">H</span> <span class="o">:</span> <span class="mi">1</span> <span class="bp">=</span> <span class="bp">-</span><span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">addarith</span> <span class="o">[</span><span class="n">hm1</span><span class="o">,</span> <span class="n">hm2</span><span class="o">]</span>
  <span class="n">numbers</span> <span class="n">at</span> <span class="n">H</span>
</pre></div>
</div>
</section>
<section id="standard-plane-bij">
<span id="id33"></span><h3><span class="section-number">8.4.2. </span>Example<a class="headerlink" href="#standard-plane-bij" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Consider the function <span class="math notranslate nohighlight">\((m,n)\mapsto (m + n, m + 2n)\)</span> from <span class="math notranslate nohighlight">\(\mathbb{Z}^2\)</span> to
<span class="math notranslate nohighlight">\(\mathbb{Z}^2\)</span>.
Show that this function is bijective.</p>
</div>
<p>Usually, the most efficient way to prove a function is bijective is to produce an inverse for it.
This is enough because of the theorem we proved in <a class="reference internal" href="#bijective-iff-inverse"><span class="std std-numref">Example 8.3.9</span></a>.
Coming up with this inverse is something you should do in rough work, probably on paper rather than
in Lean.  For example, in this problem, you can set up an equation in <span class="math notranslate nohighlight">\((a,b)\)</span> which the
inverse has to satisfy:</p>
<div class="math notranslate nohighlight">
\[(a,b)=(m+n, m+2n)\]</div>
<p>and simplify to a system of integer equations, and then solve for <span class="math notranslate nohighlight">\(m\)</span> and <span class="math notranslate nohighlight">\(n\)</span>:</p>
<div class="math notranslate nohighlight">
\[\begin{split}a&amp;=m+n\\
b&amp;=m+2n\\
b-a&amp;=(m+2n)-(m+n)\\
&amp;=n\\
n&amp;=b-a\\
a&amp;=m+n\\
&amp;=m+(b-a)\\
a-(b-a)&amp;=m\\
2a-b&amp;=m\\
m&amp;=2a-b\end{split}\]</div>
<p>to conclude that a good candidate for the inverse is the function
<span class="math notranslate nohighlight">\((a,b)\mapsto (2a-b, b-a)\)</span> from <span class="math notranslate nohighlight">\(\mathbb{Z}^2\)</span> to <span class="math notranslate nohighlight">\(\mathbb{Z}^2\)</span>.  But this rough
work does not get included in the write-up, either on paper or in Lean.  Instead, just produce the
inverse out of a hat, and check that it works.</p>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>By <a class="reference internal" href="#bijective-iff-inverse"><span class="std std-numref">Example 8.3.9</span></a> it suffices to show that this function has an
inverse.  We will show that the function <span class="math notranslate nohighlight">\((a,b)\mapsto (2a-b, b-a)\)</span> is inverse to this
function.</p>
<p>Firstly, for any <span class="math notranslate nohighlight">\((m,n)\)</span> in <span class="math notranslate nohighlight">\(\mathbb{Z}^2\)</span>, we have that</p>
<div class="math notranslate nohighlight">
\[\left(2 (m + n) - (m + 2 n), (m + 2 n) - (m + n)\right) = (m, n).\]</div>
<p>Secondly, for any <span class="math notranslate nohighlight">\((a,b)\)</span> in <span class="math notranslate nohighlight">\(\mathbb{Z}^2\)</span>, we have that</p>
<div class="math notranslate nohighlight">
\[\left((2  a - b) + (b - a), (2  a - b) + 2  (b - a)\right) = (a, b).\]</div>
</div>
<p>In Lean, note</p>
<ul class="simple">
<li><p>the lemma <code class="docutils literal notranslate"><span class="pre">bijective_iff_exists_inverse</span></code>, which is the Lean name for the theorem from
<a class="reference internal" href="#bijective-iff-inverse"><span class="std std-numref">Example 8.3.9</span></a>;</p></li>
<li><p>the use of the tactic <code class="docutils literal notranslate"><span class="pre">ext</span></code> (recall <a class="reference internal" href="#ext"><span class="std std-numref">Example 8.3.2</span></a>) to show that two functions
are equal by showing that they are equal on arbitrary input.</p></li>
</ul>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Bijective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">((</span><span class="n">m</span><span class="o">,</span> <span class="n">n</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">&#215;</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="o">(</span><span class="n">m</span> <span class="bp">+</span> <span class="n">n</span><span class="o">,</span> <span class="n">m</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">n</span><span class="o">))</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">rw</span> <span class="o">[</span><span class="n">bijective_iff_exists_inverse</span><span class="o">]</span>
  <span class="n">use</span> <span class="k">fun</span> <span class="o">(</span><span class="n">a</span><span class="o">,</span> <span class="n">b</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="o">(</span><span class="mi">2</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">-</span> <span class="n">b</span><span class="o">,</span> <span class="n">b</span> <span class="bp">-</span> <span class="n">a</span><span class="o">)</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">ext</span> <span class="o">&#10216;</span><span class="n">m</span><span class="o">,</span> <span class="n">n</span><span class="o">&#10217;</span>
    <span class="n">dsimp</span>
    <span class="n">ring</span>
  <span class="bp">&#183;</span> <span class="n">ext</span> <span class="o">&#10216;</span><span class="n">a</span><span class="o">,</span> <span class="n">b</span><span class="o">&#10217;</span>
    <span class="n">dsimp</span>
    <span class="n">ring</span>
</pre></div>
</div>
</section>
<section id="id34">
<h3><span class="section-number">8.4.3. </span>Example<a class="headerlink" href="#id34" title="Permalink to this headline">&#61633;</a></h3>
<p>The ideas of <a class="reference internal" href="#standard-plane-bij"><span class="std std-numref">Example 8.4.2</span></a> can be adapted fairly flexibly, particularly
over the rationals and over the reals.  Try this one yourself.</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Consider the function <span class="math notranslate nohighlight">\((m,n)\mapsto (m + n, m - n)\)</span> from <span class="math notranslate nohighlight">\(\mathbb{R}^2\)</span> to
<span class="math notranslate nohighlight">\(\mathbb{R}^2\)</span>.
Show that this function is bijective.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Bijective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">((</span><span class="n">m</span><span class="o">,</span> <span class="n">n</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">&#215;</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="o">(</span><span class="n">m</span> <span class="bp">+</span> <span class="n">n</span><span class="o">,</span> <span class="n">m</span> <span class="bp">-</span> <span class="n">n</span><span class="o">))</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
<p>But over the integers, complications can ensue.  You&#8217;ll find that the inverse you come up with for
the previous example involves a division, which works fine over <span class="math notranslate nohighlight">\(\mathbb{R}\)</span> but doesn&#8217;t work
over <span class="math notranslate nohighlight">\(\mathbb{Z}\)</span>.  And in fact in this case the function is <em>not</em> bijective as a map from
<span class="math notranslate nohighlight">\(\mathbb{Z}^2\)</span> to <span class="math notranslate nohighlight">\(\mathbb{Z}^2\)</span>.</p>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Consider the function <span class="math notranslate nohighlight">\((m,n)\mapsto (m + n, m - n)\)</span> from <span class="math notranslate nohighlight">\(\mathbb{Z}^2\)</span> to
<span class="math notranslate nohighlight">\(\mathbb{Z}^2\)</span>.
Show that this function is not bijective.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>We will show that the function is not surjective.  In fact, we will show that for all
<span class="math notranslate nohighlight">\((m,n)\)</span> in <span class="math notranslate nohighlight">\(\mathbb{Z}^2\)</span>, it is not true that <span class="math notranslate nohighlight">\((m + n, m - n)=(0,1)\)</span>.  So let
<span class="math notranslate nohighlight">\((m,n)\)</span> be in <span class="math notranslate nohighlight">\(\mathbb{Z}^2\)</span> and suppose that <span class="math notranslate nohighlight">\((m + n, m - n)=(0,1)\)</span>.  Then
<span class="math notranslate nohighlight">\(m+n=0\)</span> and <span class="math notranslate nohighlight">\(m-n=1\)</span>, so</p>
<div class="math notranslate nohighlight">
\[\begin{split}0&amp;\equiv 2m\mod 2\\
&amp;=(m-n)+(m+n)\\
&amp;=1+0\\
&amp;=1,\end{split}\]</div>
<p>contradiction.</p>
</div>
<p>The last part of the problem could play out in several different ways.  The hypotheses <span class="math notranslate nohighlight">\(m+n=0\)</span>
and <span class="math notranslate nohighlight">\(m-n=1\)</span> are pretty clearly contradictory (for integers), so there are several variant ways
you could produce the contradiction instead of the numeric contradiction <span class="math notranslate nohighlight">\(0\equiv 1\mod 2\)</span>
which I produced here.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Bijective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">((</span><span class="n">m</span><span class="o">,</span> <span class="n">n</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">&#215;</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="o">(</span><span class="n">m</span> <span class="bp">+</span> <span class="n">n</span><span class="o">,</span> <span class="n">m</span> <span class="bp">-</span> <span class="n">n</span><span class="o">))</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Bijective</span><span class="o">,</span> <span class="n">Injective</span><span class="o">,</span> <span class="n">Surjective</span><span class="o">]</span>
  <span class="n">push_neg</span>
  <span class="n">right</span>
  <span class="n">use</span> <span class="o">(</span><span class="mi">0</span><span class="o">,</span> <span class="mi">1</span><span class="o">)</span>
  <span class="n">intro</span> <span class="o">(</span><span class="n">m</span><span class="o">,</span> <span class="n">n</span><span class="o">)</span> <span class="n">h</span>
  <span class="n">dsimp</span> <span class="n">at</span> <span class="n">h</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">h1</span><span class="o">,</span> <span class="n">h2</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h</span>
  <span class="k">have</span> <span class="o">:=</span>
  <span class="k">calc</span> <span class="mi">0</span> <span class="bp">&#8801;</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">m</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">2</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">extra</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="o">(</span><span class="n">m</span> <span class="bp">-</span> <span class="n">n</span><span class="o">)</span> <span class="bp">+</span> <span class="o">(</span><span class="n">m</span> <span class="bp">+</span> <span class="n">n</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="mi">1</span> <span class="bp">+</span> <span class="mi">0</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">h1</span><span class="o">,</span> <span class="n">h2</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">numbers</span>
  <span class="n">numbers</span> <span class="n">at</span> <span class="n">this</span>
</pre></div>
</div>
</section>
<section id="injective-r2-r3">
<span id="id35"></span><h3><span class="section-number">8.4.4. </span>Example<a class="headerlink" href="#injective-r2-r3" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Consider the function <span class="math notranslate nohighlight">\((x,y)\mapsto (x+y,x-y, y)\)</span> from  <span class="math notranslate nohighlight">\(\mathbb{R}^2\)</span> to
<span class="math notranslate nohighlight">\(\mathbb{R}^3\)</span>. Show that this function is injective.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Let <span class="math notranslate nohighlight">\((x_1,y_1)\)</span> and <span class="math notranslate nohighlight">\((x_2,y_2)\)</span> be points in <span class="math notranslate nohighlight">\(\mathbb{R}^2\)</span> and suppose that</p>
<div class="math notranslate nohighlight">
\[(x_1+y_1,x_1-y_1, y_1)=(x_2+y_2,x_2-y_2, y_2).\]</div>
<p>Then, inspecting co-ordinate by co-ordinate, we have that</p>
<div class="math notranslate nohighlight">
\[\begin{split}x_1+y_1&amp;=x_2+y_2\\
x_1-y_1&amp;=x_2-y_2\\
y_1&amp;=y_2\end{split}\]</div>
<p>Subtracting the third equation from the first, we also have that <span class="math notranslate nohighlight">\(x_1=x_2\)</span>.  So
<span class="math notranslate nohighlight">\((x_1,y_1)=(x_2,y_2)\)</span>.</p>
</div>
<p>In Lean, note the use of the tactic <code class="docutils literal notranslate"><span class="pre">constructor</span></code> to reduce a goal of equality in a product type,</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>&#8866; (x1, y1) = (x2, y2)
</pre></div>
</div>
<p>to two simpler goals, one for each co-ordinate:</p>
<div class="highlight-text notranslate"><div class="highlight"><pre><span></span>&#8866; x1 = x2
&#8866; y1 = y2
</pre></div>
</div>
<p>As with the use of <code class="docutils literal notranslate"><span class="pre">obtain</span></code> for hypotheses of equality in a product type  (recall
<a class="reference internal" href="#obtain-product"><span class="std std-numref">Example 8.4.1</span></a>), the point is that an equality in a product type is
effectively an &#8220;and&#8221; statement about equality in the first and the second co-ordinates.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Injective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">((</span><span class="n">x</span><span class="o">,</span> <span class="n">y</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">&#215;</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="o">(</span><span class="n">x</span> <span class="bp">+</span> <span class="n">y</span><span class="o">,</span> <span class="n">x</span> <span class="bp">-</span> <span class="n">y</span><span class="o">,</span> <span class="n">y</span><span class="o">))</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">intro</span> <span class="o">(</span><span class="n">x1</span><span class="o">,</span> <span class="n">y1</span><span class="o">)</span> <span class="o">(</span><span class="n">x2</span><span class="o">,</span> <span class="n">y2</span><span class="o">)</span> <span class="n">h</span>
  <span class="n">dsimp</span> <span class="n">at</span> <span class="n">h</span>
  <span class="n">obtain</span> <span class="o">&#10216;</span><span class="n">h</span><span class="o">,</span> <span class="n">h&#39;</span><span class="o">,</span> <span class="n">hy</span><span class="o">&#10217;</span> <span class="o">:=</span> <span class="n">h</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">addarith</span> <span class="o">[</span><span class="n">h</span><span class="o">,</span> <span class="n">hy</span><span class="o">]</span>
  <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">hy</span>
</pre></div>
</div>
</section>
<section id="id36">
<h3><span class="section-number">8.4.5. </span>Example<a class="headerlink" href="#id36" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Consider the function <span class="math notranslate nohighlight">\((x,y)\mapsto x + y\)</span> from <span class="math notranslate nohighlight">\(\mathbb{R}^2\)</span> to <span class="math notranslate nohighlight">\(\mathbb{R}\)</span>.
Show that this function is</p>
<ol class="arabic simple">
<li><p>not injective;</p></li>
<li><p>surjective.</p></li>
</ol>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>1. We will show that there exist points <span class="math notranslate nohighlight">\((x_1,y_1)\)</span> and <span class="math notranslate nohighlight">\((x_2,y_2)\)</span> in
<span class="math notranslate nohighlight">\(\mathbb{R}^2\)</span> such that <span class="math notranslate nohighlight">\(x_1+y_1=x_2+y_2\)</span> and <span class="math notranslate nohighlight">\((x_1,y_1)\ne (x_2,y_2)\)</span>.
Indeed, consider the points <span class="math notranslate nohighlight">\((0,0)\)</span> and <span class="math notranslate nohighlight">\((1,-1)\)</span>.  We have that <span class="math notranslate nohighlight">\(0+0=1+-1\)</span> and
<span class="math notranslate nohighlight">\((0,0)\ne (1,-1)\)</span>.</p>
<p>2. Let <span class="math notranslate nohighlight">\(a\)</span> be a real number.  We must show that there exists a point <span class="math notranslate nohighlight">\((x,y)\)</span> in
<span class="math notranslate nohighlight">\(\mathbb{R}^2\)</span> such that <span class="math notranslate nohighlight">\(x+y=a\)</span>. Indeed, <span class="math notranslate nohighlight">\(a+0=a\)</span>, so <span class="math notranslate nohighlight">\((a,0)\)</span> has this
property.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Injective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">((</span><span class="n">x</span><span class="o">,</span> <span class="n">y</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">&#215;</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="n">x</span> <span class="bp">+</span> <span class="n">y</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Injective</span><span class="o">]</span>
  <span class="n">push_neg</span>
  <span class="n">use</span> <span class="o">(</span><span class="mi">0</span><span class="o">,</span> <span class="mi">0</span><span class="o">),</span> <span class="o">(</span><span class="mi">1</span><span class="o">,</span> <span class="bp">-</span><span class="mi">1</span><span class="o">)</span>
  <span class="n">dsimp</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">numbers</span>
  <span class="bp">&#183;</span> <span class="n">numbers</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Surjective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">((</span><span class="n">x</span><span class="o">,</span> <span class="n">y</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">&#215;</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="n">x</span> <span class="bp">+</span> <span class="n">y</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">intro</span> <span class="n">a</span>
  <span class="n">use</span> <span class="o">(</span><span class="n">a</span><span class="o">,</span> <span class="mi">0</span><span class="o">)</span>
  <span class="n">dsimp</span>
  <span class="n">ring</span>
</pre></div>
</div>
</section>
<section id="id37">
<h3><span class="section-number">8.4.6. </span>Example<a class="headerlink" href="#id37" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Consider the function <span class="math notranslate nohighlight">\((m,n)\mapsto 5m+8n\)</span> from <span class="math notranslate nohighlight">\(\mathbb{Z}^2\)</span> to <span class="math notranslate nohighlight">\(\mathbb{Z}\)</span>.
Show that this function is</p>
<ol class="arabic simple">
<li><p>not injective;</p></li>
<li><p>surjective.</p></li>
</ol>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>1. We will show that there exist pairs <span class="math notranslate nohighlight">\((m_1,n_1)\)</span> and <span class="math notranslate nohighlight">\((m_2,n_2)\)</span> in
<span class="math notranslate nohighlight">\(\mathbb{Z}^2\)</span> such that <span class="math notranslate nohighlight">\(5m_1+8n_1=5m_2+8n_2\)</span> and <span class="math notranslate nohighlight">\((m_1,n_1)\ne (m_2,n_2)\)</span>.
Indeed, consider the pairs <span class="math notranslate nohighlight">\((0,0)\)</span> and <span class="math notranslate nohighlight">\((8,-5)\)</span>.  We have that
<span class="math notranslate nohighlight">\(5\cdot 0+8\cdot 0=5\cdot 8+8\cdot -5\)</span> and
<span class="math notranslate nohighlight">\((0,0)\ne (8,-5)\)</span>.</p>
<p>2. Let <span class="math notranslate nohighlight">\(a\)</span> be an integer.  We must show that there exists a pair <span class="math notranslate nohighlight">\((m,n)\)</span> in
<span class="math notranslate nohighlight">\(\mathbb{Z}^2\)</span> such that <span class="math notranslate nohighlight">\(5m+8n=a\)</span>. Indeed, <span class="math notranslate nohighlight">\(5(-3a)+8(2a)=a\)</span>, so
<span class="math notranslate nohighlight">\((-3a,2a)\)</span> has this property.</p>
</div>
<p>(Where did the idea for the -3 and the 2 come from in the second part of this proof?  Compare with
<a class="reference internal" href="03_Parity_and_Divisibility.html#bezout-prob1"><span class="std std-numref">Example 3.5.1</span></a> and <a class="reference internal" href="03_Parity_and_Divisibility.html#bezout-prob3"><span class="std std-numref">Example 3.5.3</span></a>.)</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Injective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">((</span><span class="n">m</span><span class="o">,</span> <span class="n">n</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">&#215;</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">m</span> <span class="bp">+</span> <span class="mi">8</span> <span class="bp">*</span> <span class="n">n</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Injective</span><span class="o">]</span>
  <span class="n">push_neg</span>
  <span class="n">use</span> <span class="o">(</span><span class="mi">0</span><span class="o">,</span> <span class="mi">0</span><span class="o">),</span> <span class="o">(</span><span class="mi">8</span><span class="o">,</span> <span class="bp">-</span><span class="mi">5</span><span class="o">)</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">numbers</span>
  <span class="bp">&#183;</span> <span class="n">numbers</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Surjective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">((</span><span class="n">m</span><span class="o">,</span> <span class="n">n</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">&#215;</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">m</span> <span class="bp">+</span> <span class="mi">8</span> <span class="bp">*</span> <span class="n">n</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">intro</span> <span class="n">a</span>
  <span class="n">use</span> <span class="o">(</span><span class="bp">-</span><span class="mi">3</span> <span class="bp">*</span> <span class="n">a</span><span class="o">,</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">a</span><span class="o">)</span>
  <span class="n">dsimp</span>
  <span class="n">ring</span>
</pre></div>
</div>
</section>
<section id="id38">
<h3><span class="section-number">8.4.7. </span>Example<a class="headerlink" href="#id38" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Consider the function <span class="math notranslate nohighlight">\((m,n)\mapsto 5m+10n\)</span> from <span class="math notranslate nohighlight">\(\mathbb{Z}^2\)</span> to <span class="math notranslate nohighlight">\(\mathbb{Z}\)</span>.
Show that this function is</p>
<ol class="arabic simple">
<li><p>not injective;</p></li>
<li><p>not surjective.</p></li>
</ol>
</div>
<p>We leave the non-injectivity proof as an exercise; it is similar to that in the previous two problems.</p>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>(Non-surjectivity) We will show that there exists an integer <span class="math notranslate nohighlight">\(x\)</span> such that for all pairs <span class="math notranslate nohighlight">\((m,n)\)</span>
of integers, <span class="math notranslate nohighlight">\(5m+10n\ne x\)</span>.  Indeed, let us show that 1 has this property.  Let
<span class="math notranslate nohighlight">\((m,n)\)</span> be a pair of integers and suppose that <span class="math notranslate nohighlight">\(5m+10n=1\)</span>.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}0 &amp;\equiv 5(m+2n)\mod 5\\
&amp;=5m+10n\\
&amp;=1,\end{split}\]</div>
<p>contradiction.</p>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Injective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">((</span><span class="n">m</span><span class="o">,</span> <span class="n">n</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">&#215;</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">m</span> <span class="bp">+</span> <span class="mi">10</span> <span class="bp">*</span> <span class="n">n</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>

<span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Surjective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">((</span><span class="n">m</span><span class="o">,</span> <span class="n">n</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">&#215;</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">m</span> <span class="bp">+</span> <span class="mi">10</span> <span class="bp">*</span> <span class="n">n</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">Surjective</span><span class="o">]</span>
  <span class="n">push_neg</span>
  <span class="n">use</span> <span class="mi">1</span>
  <span class="n">intro</span> <span class="o">(</span><span class="n">m</span><span class="o">,</span> <span class="n">n</span><span class="o">)</span> <span class="n">h</span>
  <span class="n">dsimp</span> <span class="n">at</span> <span class="n">h</span>
  <span class="k">have</span> <span class="o">:=</span>
  <span class="k">calc</span> <span class="mi">0</span> <span class="bp">&#8801;</span> <span class="mi">5</span> <span class="bp">*</span> <span class="o">(</span><span class="n">m</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">n</span><span class="o">)</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">extra</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">m</span> <span class="bp">+</span> <span class="mi">10</span> <span class="bp">*</span> <span class="n">n</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="mi">1</span> <span class="o">:=</span> <span class="n">h</span>
  <span class="n">numbers</span> <span class="n">at</span> <span class="n">this</span>
</pre></div>
</div>
</section>
<section id="id39">
<h3><span class="section-number">8.4.8. </span>Example<a class="headerlink" href="#id39" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-problem admonition">
<p class="admonition-title">Problem</p>
<p>Consider the function <span class="math notranslate nohighlight">\(g:\mathbb{R}^2\to \mathbb{R}^2\)</span> defined by,
<span class="math notranslate nohighlight">\(g(x,y)=(y,x)\)</span>.  Show that <span class="math notranslate nohighlight">\(g\circ g=\operatorname{Id}_\mathbb{R}\)</span>.</p>
</div>
<div class="admonition-solution admonition">
<p class="admonition-title">Solution</p>
<p>Let <span class="math notranslate nohighlight">\((x,y)\)</span> be a point in <span class="math notranslate nohighlight">\(\mathbb{R}^2\)</span>.  Then</p>
<div class="math notranslate nohighlight">
\[\begin{split}g(g(x,y))&amp;=g(y,x)\\
&amp;=(x,y).\end{split}\]</div>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">g</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">&#215;</span> <span class="n">&#8477;</span> <span class="bp">&#8594;</span> <span class="n">&#8477;</span> <span class="bp">&#215;</span> <span class="n">&#8477;</span>
  <span class="bp">|</span> <span class="o">(</span><span class="n">x</span><span class="o">,</span> <span class="n">y</span><span class="o">)</span> <span class="bp">=&gt;</span> <span class="o">(</span><span class="n">y</span><span class="o">,</span> <span class="n">x</span><span class="o">)</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">g</span> <span class="bp">&#8728;</span> <span class="n">g</span> <span class="bp">=</span> <span class="n">id</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">ext</span> <span class="o">&#10216;</span><span class="n">x</span><span class="o">,</span> <span class="n">y</span><span class="o">&#10217;</span>
  <span class="n">dsimp</span> <span class="o">[</span><span class="n">g</span><span class="o">]</span>
</pre></div>
</div>
</section>
<section id="id40">
<h3><span class="section-number">8.4.9. </span>Example<a class="headerlink" href="#id40" title="Permalink to this headline">&#61633;</a></h3>
<div class="admonition-theorem admonition">
<p class="admonition-title">Theorem</p>
<p>There exists a bijection from <span class="math notranslate nohighlight">\(\mathbb{N}^2\)</span> to <span class="math notranslate nohighlight">\(\mathbb{N}\)</span>.</p>
</div>
<p>First recall the sequence <span class="math notranslate nohighlight">\(A_n\)</span> from <a class="reference internal" href="06_Induction.html#triangle"><span class="std std-numref">Example 6.2.4</span></a>; we prove a lemma about
it.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">A</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">&#8469;</span>
  <span class="bp">|</span> <span class="mi">0</span> <span class="bp">=&gt;</span> <span class="mi">0</span>
  <span class="bp">|</span> <span class="n">n</span> <span class="bp">+</span> <span class="mi">1</span> <span class="bp">=&gt;</span> <span class="n">A</span> <span class="n">n</span> <span class="bp">+</span> <span class="n">n</span> <span class="bp">+</span> <span class="mi">1</span>

<span class="kd">theorem</span> <span class="n">A_mono</span> <span class="o">{</span><span class="n">n</span> <span class="n">m</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">}</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">n</span> <span class="bp">&#8804;</span> <span class="n">m</span><span class="o">)</span> <span class="o">:</span> <span class="n">A</span> <span class="n">n</span> <span class="bp">&#8804;</span> <span class="n">A</span> <span class="n">m</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">induction_from_starting_point</span> <span class="n">m</span><span class="o">,</span> <span class="n">h</span> <span class="k">with</span> <span class="n">k</span> <span class="n">hk</span> <span class="n">IH</span>
  <span class="bp">&#183;</span> <span class="n">extra</span>
  <span class="bp">&#183;</span> <span class="k">calc</span> <span class="n">A</span> <span class="n">n</span> <span class="bp">&#8804;</span> <span class="n">A</span> <span class="n">k</span> <span class="o">:=</span> <span class="n">IH</span>
      <span class="n">_</span> <span class="bp">&#8804;</span> <span class="n">A</span> <span class="n">k</span> <span class="bp">+</span> <span class="o">(</span><span class="n">k</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">extra</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="n">A</span> <span class="n">k</span> <span class="bp">+</span> <span class="n">k</span> <span class="bp">+</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="n">A</span> <span class="o">(</span><span class="n">k</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">A</span><span class="o">]</span>
</pre></div>
</div>
<p>And a corollary, more difficult.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">of_A_add_mono</span> <span class="o">{</span><span class="n">a1</span> <span class="n">a2</span> <span class="n">b1</span> <span class="n">b2</span> <span class="o">:</span> <span class="n">&#8469;</span><span class="o">}</span> <span class="o">(</span><span class="n">h</span> <span class="o">:</span> <span class="n">A</span> <span class="o">(</span><span class="n">a1</span> <span class="bp">+</span> <span class="n">b1</span><span class="o">)</span> <span class="bp">+</span> <span class="n">b1</span> <span class="bp">&#8804;</span> <span class="n">A</span> <span class="o">(</span><span class="n">a2</span> <span class="bp">+</span> <span class="n">b2</span><span class="o">)</span> <span class="bp">+</span> <span class="n">b2</span><span class="o">)</span> <span class="o">:</span>
    <span class="n">a1</span> <span class="bp">+</span> <span class="n">b1</span> <span class="bp">&#8804;</span> <span class="n">a2</span> <span class="bp">+</span> <span class="n">b2</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">obtain</span> <span class="n">h&#39;</span> <span class="bp">|</span> <span class="n">h&#39;</span> <span class="o">:</span> <span class="n">_</span> <span class="bp">&#8744;</span> <span class="n">a2</span> <span class="bp">+</span> <span class="n">b2</span> <span class="bp">+</span> <span class="mi">1</span> <span class="bp">&#8804;</span> <span class="n">a1</span> <span class="bp">+</span> <span class="n">b1</span> <span class="o">:=</span> <span class="n">le_or_lt</span> <span class="o">(</span><span class="n">a1</span> <span class="bp">+</span> <span class="n">b1</span><span class="o">)</span> <span class="o">(</span><span class="n">a2</span> <span class="bp">+</span> <span class="n">b2</span><span class="o">)</span>
  <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">h&#39;</span>
  <span class="n">rw</span> <span class="o">[</span><span class="bp">&#8592;</span> <span class="n">not_lt</span><span class="o">]</span> <span class="n">at</span> <span class="n">h</span>
  <span class="k">have</span> <span class="o">:=</span>
  <span class="k">calc</span> <span class="n">A</span> <span class="o">(</span><span class="n">a2</span> <span class="bp">+</span> <span class="n">b2</span><span class="o">)</span> <span class="bp">+</span> <span class="n">b2</span>
     <span class="bp">&lt;</span> <span class="n">A</span> <span class="o">(</span><span class="n">a2</span> <span class="bp">+</span> <span class="n">b2</span><span class="o">)</span> <span class="bp">+</span> <span class="n">b2</span> <span class="bp">+</span> <span class="o">(</span><span class="n">a2</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">extra</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="n">A</span> <span class="o">(</span><span class="n">a2</span> <span class="bp">+</span> <span class="n">b2</span><span class="o">)</span> <span class="bp">+</span> <span class="o">(</span><span class="n">a2</span> <span class="bp">+</span> <span class="n">b2</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="n">A</span> <span class="o">((</span><span class="n">a2</span> <span class="bp">+</span> <span class="n">b2</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">A</span><span class="o">]</span>
    <span class="n">_</span> <span class="bp">=</span> <span class="n">A</span> <span class="o">(</span><span class="n">a2</span> <span class="bp">+</span> <span class="n">b2</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
    <span class="n">_</span> <span class="bp">&#8804;</span> <span class="n">A</span> <span class="o">(</span><span class="n">a1</span> <span class="bp">+</span> <span class="n">b1</span><span class="o">)</span> <span class="o">:=</span> <span class="n">A_mono</span> <span class="n">h&#39;</span>
    <span class="n">_</span> <span class="bp">&#8804;</span> <span class="n">A</span> <span class="o">(</span><span class="n">a1</span> <span class="bp">+</span> <span class="n">b1</span><span class="o">)</span> <span class="bp">+</span> <span class="n">b1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">extra</span>
  <span class="n">contradiction</span>
</pre></div>
</div>
<p>We use the sequence <span class="math notranslate nohighlight">\(A_n\)</span> to define the function <span class="math notranslate nohighlight">\(p:\mathbb{N}^2\to \mathbb{N}\)</span> which
will be the bijection we seek:  <span class="math notranslate nohighlight">\(p(a,b)=A_{a+b}+b\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">p</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#215;</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">&#8469;</span>
  <span class="bp">|</span> <span class="o">(</span><span class="n">a</span><span class="o">,</span> <span class="n">b</span><span class="o">)</span> <span class="bp">=&gt;</span> <span class="n">A</span> <span class="o">(</span><span class="n">a</span> <span class="bp">+</span> <span class="n">b</span><span class="o">)</span> <span class="bp">+</span> <span class="n">b</span>
</pre></div>
</div>
<p>Finally we prove that this function <span class="math notranslate nohighlight">\(p\)</span> is indeed bijective.  We set up an &#8220;intertwining&#8221;
map <span class="math notranslate nohighlight">\(i\)</span> for <span class="math notranslate nohighlight">\(p\)</span>, and invoke the lemma <code class="docutils literal notranslate"><span class="pre">surjective_of_intertwining</span></code> proved in the exercises
to <a class="reference internal" href="#inj-surj"><span class="std std-numref">Section 8.1</span></a>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">i</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#215;</span> <span class="n">&#8469;</span> <span class="bp">&#8594;</span> <span class="n">&#8469;</span> <span class="bp">&#215;</span> <span class="n">&#8469;</span>
  <span class="bp">|</span> <span class="o">(</span><span class="mi">0</span><span class="o">,</span> <span class="n">b</span><span class="o">)</span> <span class="bp">=&gt;</span> <span class="o">(</span><span class="n">b</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">,</span> <span class="mi">0</span><span class="o">)</span>
  <span class="bp">|</span> <span class="o">(</span><span class="n">a</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">,</span> <span class="n">b</span><span class="o">)</span> <span class="bp">=&gt;</span> <span class="o">(</span><span class="n">a</span><span class="o">,</span> <span class="n">b</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span>

<span class="kd">theorem</span> <span class="n">p_comp_i</span> <span class="o">(</span><span class="n">x</span> <span class="o">:</span> <span class="n">&#8469;</span> <span class="bp">&#215;</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="o">:</span> <span class="n">p</span> <span class="o">(</span><span class="n">i</span> <span class="n">x</span><span class="o">)</span> <span class="bp">=</span> <span class="n">p</span> <span class="n">x</span> <span class="bp">+</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="k">match</span> <span class="n">x</span> <span class="k">with</span>
  <span class="bp">|</span> <span class="o">(</span><span class="mi">0</span><span class="o">,</span> <span class="n">b</span><span class="o">)</span> <span class="bp">=&gt;</span>
    <span class="k">calc</span> <span class="n">p</span> <span class="o">(</span><span class="n">i</span> <span class="o">(</span><span class="mi">0</span><span class="o">,</span> <span class="n">b</span><span class="o">))</span> <span class="bp">=</span> <span class="n">p</span> <span class="o">(</span><span class="n">b</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">,</span> <span class="mi">0</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">i</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="n">A</span> <span class="o">((</span><span class="n">b</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">0</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">0</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">dsimp</span> <span class="o">[</span><span class="n">p</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="n">A</span> <span class="o">(</span><span class="n">b</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="n">A</span> <span class="n">b</span> <span class="bp">+</span> <span class="n">b</span> <span class="bp">+</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">A</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="o">(</span><span class="n">A</span> <span class="o">(</span><span class="mi">0</span> <span class="bp">+</span> <span class="n">b</span><span class="o">)</span> <span class="bp">+</span> <span class="n">b</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="n">p</span> <span class="o">(</span><span class="mi">0</span><span class="o">,</span> <span class="n">b</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">dsimp</span> <span class="o">[</span><span class="n">p</span><span class="o">]</span>
  <span class="bp">|</span> <span class="o">(</span><span class="n">a</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">,</span> <span class="n">b</span><span class="o">)</span> <span class="bp">=&gt;</span>
    <span class="k">calc</span> <span class="n">p</span> <span class="o">(</span><span class="n">i</span> <span class="o">(</span><span class="n">a</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">,</span> <span class="n">b</span><span class="o">))</span> <span class="bp">=</span> <span class="n">p</span> <span class="o">(</span><span class="n">a</span><span class="o">,</span> <span class="n">b</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">i</span><span class="o">]</span> <span class="bp">;</span> <span class="n">rfl</span> <span class="c1">-- FIXME</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="n">A</span> <span class="o">(</span><span class="n">a</span> <span class="bp">+</span> <span class="o">(</span><span class="n">b</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">))</span> <span class="bp">+</span> <span class="o">(</span><span class="n">b</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">dsimp</span> <span class="o">[</span><span class="n">p</span><span class="o">]</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="o">(</span><span class="n">A</span> <span class="o">((</span><span class="n">a</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">)</span> <span class="bp">+</span> <span class="n">b</span><span class="o">)</span> <span class="bp">+</span> <span class="n">b</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
      <span class="n">_</span> <span class="bp">=</span> <span class="n">p</span> <span class="o">(</span><span class="n">a</span> <span class="bp">+</span> <span class="mi">1</span><span class="o">,</span> <span class="n">b</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">1</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">p</span><span class="o">]</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">Bijective</span> <span class="n">p</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">constructor</span>
  <span class="bp">&#183;</span> <span class="n">intro</span> <span class="o">(</span><span class="n">a1</span><span class="o">,</span> <span class="n">b1</span><span class="o">)</span> <span class="o">(</span><span class="n">a2</span><span class="o">,</span> <span class="n">b2</span><span class="o">)</span> <span class="n">hab</span>
    <span class="n">dsimp</span> <span class="o">[</span><span class="n">p</span><span class="o">]</span> <span class="n">at</span> <span class="n">hab</span>
    <span class="k">have</span> <span class="n">H</span> <span class="o">:</span> <span class="n">a1</span> <span class="bp">+</span> <span class="n">b1</span> <span class="bp">=</span> <span class="n">a2</span> <span class="bp">+</span> <span class="n">b2</span>
    <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">le_antisymm</span>
      <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">of_A_add_mono</span>
        <span class="n">rw</span> <span class="o">[</span><span class="n">hab</span><span class="o">]</span>
      <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">of_A_add_mono</span>
        <span class="n">rw</span> <span class="o">[</span><span class="n">hab</span><span class="o">]</span>
    <span class="k">have</span> <span class="n">hb</span> <span class="o">:</span> <span class="n">b1</span> <span class="bp">=</span> <span class="n">b2</span>
    <span class="bp">&#183;</span> <span class="n">zify</span> <span class="n">at</span> <span class="n">hab</span> <span class="bp">&#8866;</span>
      <span class="k">calc</span> <span class="o">(</span><span class="n">b1</span><span class="o">:</span><span class="n">&#8484;</span><span class="o">)</span> <span class="bp">=</span> <span class="n">A</span> <span class="o">(</span><span class="n">a2</span> <span class="bp">+</span> <span class="n">b2</span><span class="o">)</span> <span class="bp">+</span> <span class="n">b2</span> <span class="bp">-</span> <span class="n">A</span> <span class="o">(</span><span class="n">a1</span> <span class="bp">+</span> <span class="n">b1</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">addarith</span> <span class="o">[</span><span class="n">hab</span><span class="o">]</span>
        <span class="n">_</span> <span class="bp">=</span> <span class="n">A</span> <span class="o">(</span><span class="n">a2</span> <span class="bp">+</span> <span class="n">b2</span><span class="o">)</span> <span class="bp">+</span> <span class="n">b2</span> <span class="bp">-</span> <span class="n">A</span> <span class="o">(</span><span class="n">a2</span> <span class="bp">+</span> <span class="n">b2</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">H</span><span class="o">]</span>
        <span class="n">_</span> <span class="bp">=</span> <span class="n">b2</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
    <span class="n">constructor</span>
    <span class="bp">&#183;</span> <span class="n">zify</span> <span class="n">at</span> <span class="n">hb</span> <span class="n">H</span> <span class="bp">&#8866;</span>
      <span class="n">addarith</span> <span class="o">[</span><span class="n">H</span><span class="o">,</span> <span class="n">hb</span><span class="o">]</span>
    <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">hb</span>
  <span class="bp">&#183;</span> <span class="n">apply</span> <span class="n">surjective_of_intertwining</span> <span class="o">(</span><span class="n">x0</span> <span class="o">:=</span> <span class="o">(</span><span class="mi">0</span><span class="o">,</span> <span class="mi">0</span><span class="o">))</span> <span class="o">(</span><span class="n">i</span> <span class="o">:=</span> <span class="n">i</span><span class="o">)</span>
    <span class="bp">&#183;</span> <span class="k">calc</span> <span class="n">p</span> <span class="o">(</span><span class="mi">0</span><span class="o">,</span> <span class="mi">0</span><span class="o">)</span> <span class="bp">=</span> <span class="n">A</span> <span class="o">(</span><span class="mi">0</span> <span class="bp">+</span> <span class="mi">0</span><span class="o">)</span> <span class="bp">+</span> <span class="mi">0</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">dsimp</span> <span class="o">[</span><span class="n">p</span><span class="o">]</span>
        <span class="n">_</span> <span class="bp">=</span> <span class="n">A</span> <span class="mi">0</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">ring</span>
        <span class="n">_</span> <span class="bp">=</span> <span class="mi">0</span> <span class="o">:=</span> <span class="kd">by</span> <span class="n">rw</span> <span class="o">[</span><span class="n">A</span><span class="o">]</span>
    <span class="bp">&#183;</span> <span class="n">intro</span> <span class="n">x</span>
      <span class="n">apply</span> <span class="n">p_comp_i</span>
</pre></div>
</div>
</section>
<section id="id41">
<h3><span class="section-number">8.4.10. </span>Exercises<a class="headerlink" href="#id41" title="Permalink to this headline">&#61633;</a></h3>
<ol class="arabic">
<li><p>Consider the function <span class="math notranslate nohighlight">\((r,s)\mapsto (s, r-s)\)</span> from <span class="math notranslate nohighlight">\(\mathbb{Q}^2\)</span> to
<span class="math notranslate nohighlight">\(\mathbb{Q}^2\)</span>.
Show that this function is bijective.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Bijective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">((</span><span class="n">r</span><span class="o">,</span> <span class="n">s</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8474;</span> <span class="bp">&#215;</span> <span class="n">&#8474;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="o">(</span><span class="n">s</span><span class="o">,</span> <span class="n">r</span> <span class="bp">-</span> <span class="n">s</span><span class="o">))</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="n">rw</span> <span class="o">[</span><span class="n">bijective_iff_exists_inverse</span><span class="o">]</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Consider the function <span class="math notranslate nohighlight">\((x,y)\mapsto x-2y-1\)</span> from <span class="math notranslate nohighlight">\(\mathbb{Z}^2\)</span> to
<span class="math notranslate nohighlight">\(\mathbb{Z}\)</span>.
Show that this function is</p>
<ol class="arabic simple">
<li><p>not injective;</p></li>
<li><p>surjective.</p></li>
</ol>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Injective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">((</span><span class="n">x</span><span class="o">,</span> <span class="n">y</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">&#215;</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="n">x</span> <span class="bp">-</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">y</span> <span class="bp">-</span> <span class="mi">1</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Surjective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">((</span><span class="n">x</span><span class="o">,</span> <span class="n">y</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">&#215;</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="n">x</span> <span class="bp">-</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">y</span> <span class="bp">-</span> <span class="mi">1</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Consider the function <span class="math notranslate nohighlight">\((x,y)\mapsto x^2+y^2\)</span> from <span class="math notranslate nohighlight">\(\mathbb{Q}^2\)</span> to
<span class="math notranslate nohighlight">\(\mathbb{Q}\)</span>.
Show that this function is not surjective.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Surjective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">((</span><span class="n">x</span><span class="o">,</span> <span class="n">y</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8474;</span> <span class="bp">&#215;</span> <span class="n">&#8474;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="n">y</span> <span class="bp">^</span> <span class="mi">2</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Consider the function <span class="math notranslate nohighlight">\((x,y)\mapsto x^2-y^2\)</span> from <span class="math notranslate nohighlight">\(\mathbb{Q}^2\)</span> to
<span class="math notranslate nohighlight">\(\mathbb{Q}\)</span>.
Show that this function is surjective.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Surjective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">((</span><span class="n">x</span><span class="o">,</span> <span class="n">y</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8474;</span> <span class="bp">&#215;</span> <span class="n">&#8474;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="n">x</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">-</span> <span class="n">y</span> <span class="bp">^</span> <span class="mi">2</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Consider the function <span class="math notranslate nohighlight">\((a,b)\mapsto a^b\)</span> from <span class="math notranslate nohighlight">\(\mathbb{Q}&#215; \mathbb{N}\)</span> to
<span class="math notranslate nohighlight">\(\mathbb{Q}\)</span>. Show that this function is surjective.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Surjective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">((</span><span class="n">a</span><span class="o">,</span> <span class="n">b</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8474;</span> <span class="bp">&#215;</span> <span class="n">&#8469;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="n">a</span> <span class="bp">^</span> <span class="n">b</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Consider the function <span class="math notranslate nohighlight">\((x,y,z)\mapsto (x+y+z,x+2y+3z)\)</span> from  <span class="math notranslate nohighlight">\(\mathbb{R}^3\)</span> to
<span class="math notranslate nohighlight">\(\mathbb{R}^2\)</span>. Show that this function is not injective.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Injective</span>
    <span class="o">(</span><span class="k">fun</span> <span class="o">((</span><span class="n">x</span><span class="o">,</span> <span class="n">y</span><span class="o">,</span> <span class="n">z</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">&#215;</span> <span class="n">&#8477;</span> <span class="bp">&#215;</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="o">(</span><span class="n">x</span> <span class="bp">+</span> <span class="n">y</span> <span class="bp">+</span> <span class="n">z</span><span class="o">,</span> <span class="n">x</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">y</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">z</span><span class="o">))</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Consider the function <span class="math notranslate nohighlight">\((x,y)\mapsto (x+y,x+2y, x+3y)\)</span> from  <span class="math notranslate nohighlight">\(\mathbb{R}^2\)</span> to
<span class="math notranslate nohighlight">\(\mathbb{R}^3\)</span>. Show that this function is injective.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="n">Injective</span> <span class="o">(</span><span class="k">fun</span> <span class="o">((</span><span class="n">x</span><span class="o">,</span> <span class="n">y</span><span class="o">)</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">&#215;</span> <span class="n">&#8477;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="o">(</span><span class="n">x</span> <span class="bp">+</span> <span class="n">y</span><span class="o">,</span> <span class="n">x</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">y</span><span class="o">,</span> <span class="n">x</span> <span class="bp">+</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">y</span><span class="o">))</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
<li><p>Consider the function <span class="math notranslate nohighlight">\(h:\mathbb{R}^3\to \mathbb{R}^3\)</span> defined by,
<span class="math notranslate nohighlight">\(h(x,y,z)=(y,z,x)\)</span>.  Show that <span class="math notranslate nohighlight">\(h\circ h\circ h=\operatorname{Id}_\mathbb{R}\)</span>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span> <span class="n">h</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">&#215;</span> <span class="n">&#8477;</span> <span class="bp">&#215;</span> <span class="n">&#8477;</span> <span class="bp">&#8594;</span> <span class="n">&#8477;</span> <span class="bp">&#215;</span> <span class="n">&#8477;</span> <span class="bp">&#215;</span> <span class="n">&#8477;</span>
  <span class="bp">|</span> <span class="o">(</span><span class="n">x</span><span class="o">,</span> <span class="n">y</span><span class="o">,</span> <span class="n">z</span><span class="o">)</span> <span class="bp">=&gt;</span> <span class="o">(</span><span class="n">y</span><span class="o">,</span> <span class="n">z</span><span class="o">,</span> <span class="n">x</span><span class="o">)</span>

<span class="kd">example</span> <span class="o">:</span> <span class="n">h</span> <span class="bp">&#8728;</span> <span class="n">h</span> <span class="bp">&#8728;</span> <span class="n">h</span> <span class="bp">=</span> <span class="n">id</span> <span class="o">:=</span> <span class="kd">by</span>
  <span class="gr">sorry</span>
</pre></div>
</div>
</li>
</ol>
</section>
</section>
</section>


           </div>
          </div>
          <footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
        <a href="07_Number_Theory.html" class="btn btn-neutral float-left" title="7. Number theory" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
        <a href="09_Sets.html" class="btn btn-neutral float-right" title="9. Sets" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
    </div>

  <hr/>

  <div role="contentinfo">
    <p>&#169; Copyright 2022-2024, Heather Macbeth.  All rights reserved.</p>
  </div>

  Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
    <a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
    provided by <a href="https://readthedocs.org">Read the Docs</a>.
   

</footer>
        </div>
      </div>
    </section>
  </div>
  <script>
      jQuery(function () {
          SphinxRtdTheme.Navigation.enable(true);
      });
  </script> 

</body>
</html>